[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{?u.898, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.947, u_3} E
⊢ Nonempty
    (IsEquivalence
      (Localization.Construction.lift (MorphismProperty.Q W)
        (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W))))
[PROOFSTEP]
suffices Localization.Construction.lift W.Q W.Q_inverts = 𝟭 _
  by
  apply Nonempty.intro
  rw [this]
  infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{?u.898, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.947, u_3} E
this :
  Localization.Construction.lift (MorphismProperty.Q W) (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)) =
    𝟭 (MorphismProperty.Localization W)
⊢ Nonempty
    (IsEquivalence
      (Localization.Construction.lift (MorphismProperty.Q W)
        (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W))))
[PROOFSTEP]
apply Nonempty.intro
[GOAL]
case val
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{?u.898, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.947, u_3} E
this :
  Localization.Construction.lift (MorphismProperty.Q W) (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)) =
    𝟭 (MorphismProperty.Localization W)
⊢ IsEquivalence
    (Localization.Construction.lift (MorphismProperty.Q W) (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)))
[PROOFSTEP]
rw [this]
[GOAL]
case val
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{?u.898, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.947, u_3} E
this :
  Localization.Construction.lift (MorphismProperty.Q W) (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)) =
    𝟭 (MorphismProperty.Localization W)
⊢ IsEquivalence (𝟭 (MorphismProperty.Localization W))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{?u.898, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.947, u_3} E
⊢ Localization.Construction.lift (MorphismProperty.Q W) (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)) =
    𝟭 (MorphismProperty.Localization W)
[PROOFSTEP]
apply Localization.Construction.uniq
[GOAL]
case h
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{?u.898, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.947, u_3} E
⊢ MorphismProperty.Q W ⋙
      Localization.Construction.lift (MorphismProperty.Q W)
        (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)) =
    MorphismProperty.Q W ⋙ 𝟭 (MorphismProperty.Localization W)
[PROOFSTEP]
simp only [Localization.Construction.fac]
[GOAL]
case h
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{?u.898, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.947, u_3} E
⊢ MorphismProperty.Q W = MorphismProperty.Q W ⋙ 𝟭 (MorphismProperty.Localization W)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.5348, u_1} C
inst✝¹ : Category.{?u.5352, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.5401, u_3} E
hW : W ⊆ MorphismProperty.isomorphisms C
F : C ⥤ E
hF : MorphismProperty.IsInvertedBy W F
⊢ 𝟭 C ⋙ (fun F x => F) F hF = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.5348, u_1} C
inst✝¹ : Category.{?u.5352, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.5401, u_3} E
hW : W ⊆ MorphismProperty.isomorphisms C
toPrefunctor✝ : C ⥤q E
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
hF : MorphismProperty.IsInvertedBy W (Functor.mk toPrefunctor✝)
⊢ 𝟭 C ⋙ (fun F x => F) (Functor.mk toPrefunctor✝) hF = Functor.mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.5348, u_1} C
inst✝¹ : Category.{?u.5352, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.5401, u_3} E
hW : W ⊆ MorphismProperty.isomorphisms C
F₁ F₂ : C ⥤ E
eq : 𝟭 C ⋙ F₁ = 𝟭 C ⋙ F₂
⊢ F₁ = F₂
[PROOFSTEP]
cases F₁
[GOAL]
case mk
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.5348, u_1} C
inst✝¹ : Category.{?u.5352, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.5401, u_3} E
hW : W ⊆ MorphismProperty.isomorphisms C
F₂ : C ⥤ E
toPrefunctor✝ : C ⥤q E
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
eq : 𝟭 C ⋙ Functor.mk toPrefunctor✝ = 𝟭 C ⋙ F₂
⊢ Functor.mk toPrefunctor✝ = F₂
[PROOFSTEP]
cases F₂
[GOAL]
case mk.mk
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.5348, u_1} C
inst✝¹ : Category.{?u.5352, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.5401, u_3} E
hW : W ⊆ MorphismProperty.isomorphisms C
toPrefunctor✝¹ : C ⥤q E
map_id✝¹ : ∀ (X : C), toPrefunctor✝¹.map (𝟙 X) = 𝟙 (toPrefunctor✝¹.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝¹.map (f ≫ g) = toPrefunctor✝¹.map f ≫ toPrefunctor✝¹.map g
toPrefunctor✝ : C ⥤q E
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
eq : 𝟭 C ⋙ Functor.mk toPrefunctor✝¹ = 𝟭 C ⋙ Functor.mk toPrefunctor✝
⊢ Functor.mk toPrefunctor✝¹ = Functor.mk toPrefunctor✝
[PROOFSTEP]
exact eq
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.6348, u_3} E
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W (MorphismProperty.Localization W)
⊢ MorphismProperty.Q W ⋙ 𝟭 (MorphismProperty.Localization W) =
    MorphismProperty.Q W ⋙
      Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙
        Localization.StrictUniversalPropertyFixedTarget.lift h₂ (MorphismProperty.Q W)
          (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W))
[PROOFSTEP]
simp only [← Functor.assoc, Localization.Construction.fac, h₂.fac, Functor.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.6348, u_3} E
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W (MorphismProperty.Localization W)
⊢ L ⋙
      Localization.StrictUniversalPropertyFixedTarget.lift h₂ (MorphismProperty.Q W)
          (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)) ⋙
        Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) =
    L ⋙ 𝟭 D
[PROOFSTEP]
simp only [← Functor.assoc, h₂.fac, Localization.Construction.fac, Functor.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.6348, u_3} E
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W (MorphismProperty.Localization W)
X : MorphismProperty.Localization W
⊢ (Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)).map
        (NatTrans.app
          (eqToIso
              (_ :
                𝟭 (MorphismProperty.Localization W) =
                  Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙
                    Localization.StrictUniversalPropertyFixedTarget.lift h₂ (MorphismProperty.Q W)
                      (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)))).hom
          X) ≫
      NatTrans.app
        (eqToIso
            (_ :
              Localization.StrictUniversalPropertyFixedTarget.lift h₂ (MorphismProperty.Q W)
                    (_ : MorphismProperty.IsInvertedBy W (MorphismProperty.Q W)) ⋙
                  Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) =
                𝟭 D)).hom
        ((Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)).obj X) =
    𝟙 ((Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)).obj X)
[PROOFSTEP]
simp only [eqToIso.hom, eqToHom_app, eqToHom_map, eqToHom_trans, eqToHom_refl]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_1, u_1} C
inst✝¹ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.6348, u_3} E
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W (MorphismProperty.Localization W)
X : MorphismProperty.Localization W
⊢ 𝟙
      ((Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)).obj
        ((𝟭 (MorphismProperty.Localization W)).obj X)) =
    𝟙 ((Localization.Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)).obj X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ IsEquivalence (whiskeringLeftFunctor L W E)
[PROOFSTEP]
refine'
  IsEquivalence.ofIso _
    (IsEquivalence.ofEquivalence
      ((Equivalence.congrLeft (equivalenceFromModel L W).symm).trans (Construction.whiskeringLeftEquivalence W E)))
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ (Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
        (Construction.whiskeringLeftEquivalence W E)).functor ≅
    whiskeringLeftFunctor L W E
[PROOFSTEP]
exact
  NatIso.ofComponents
    (fun F =>
      eqToIso
        (by
          ext
          change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F
          rw [Construction.fac]))
    fun τ => by
    ext
    dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]
    erw [NatTrans.comp_app, NatTrans.comp_app, eqToHom_app, eqToHom_app, eqToHom_refl, eqToHom_refl, comp_id, id_comp]
    · rfl
    all_goals
      change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ _ = L ⋙ _
      rw [Construction.fac]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
F : D ⥤ E
⊢ (Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
            (Construction.whiskeringLeftEquivalence W E)).functor.obj
      F =
    (whiskeringLeftFunctor L W E).obj F
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
F : D ⥤ E
⊢ ((Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
              (Construction.whiskeringLeftEquivalence W E)).functor.obj
        F).obj =
    ((whiskeringLeftFunctor L W E).obj F).obj
[PROOFSTEP]
change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F
[GOAL]
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
F : D ⥤ E
⊢ (MorphismProperty.Q W ⋙ Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)) ⋙ F = L ⋙ F
[PROOFSTEP]
rw [Construction.fac]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
⊢ (Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
              (Construction.whiskeringLeftEquivalence W E)).functor.map
        τ ≫
      ((fun F =>
            eqToIso
              (_ :
                (Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
                          (Construction.whiskeringLeftEquivalence W E)).functor.obj
                    F =
                  (whiskeringLeftFunctor L W E).obj F))
          Y✝).hom =
    ((fun F =>
            eqToIso
              (_ :
                (Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
                          (Construction.whiskeringLeftEquivalence W E)).functor.obj
                    F =
                  (whiskeringLeftFunctor L W E).obj F))
          X✝).hom ≫
      (whiskeringLeftFunctor L W E).map τ
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app
      ((Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
                (Construction.whiskeringLeftEquivalence W E)).functor.map
          τ ≫
        ((fun F =>
              eqToIso
                (_ :
                  (Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
                            (Construction.whiskeringLeftEquivalence W E)).functor.obj
                      F =
                    (whiskeringLeftFunctor L W E).obj F))
            Y✝).hom)
      x✝ =
    NatTrans.app
      (((fun F =>
              eqToIso
                (_ :
                  (Equivalence.trans (Equivalence.congrLeft (Equivalence.symm (equivalenceFromModel L W)))
                            (Construction.whiskeringLeftEquivalence W E)).functor.obj
                      F =
                    (whiskeringLeftFunctor L W E).obj F))
            X✝).hom ≫
        (whiskeringLeftFunctor L W E).map τ)
      x✝
[PROOFSTEP]
dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]
[GOAL]
case h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app
      ((Construction.WhiskeringLeftEquivalence.functor W E).map (NatTrans.mk fun X => NatTrans.app τ (L.obj X.as.obj)) ≫
        eqToHom
          (_ :
            (Construction.WhiskeringLeftEquivalence.functor W E).obj
                (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ Y✝) =
              (whiskeringLeftFunctor L W E).obj Y✝))
      x✝ =
    NatTrans.app
      (eqToHom
          (_ :
            (Construction.WhiskeringLeftEquivalence.functor W E).obj
                (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ X✝) =
              (whiskeringLeftFunctor L W E).obj X✝) ≫
        (whiskeringLeftFunctor L W E).map τ)
      x✝
[PROOFSTEP]
erw [NatTrans.comp_app, NatTrans.comp_app, eqToHom_app, eqToHom_app, eqToHom_refl, eqToHom_refl, comp_id, id_comp]
[GOAL]
case h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app
      ((Construction.WhiskeringLeftEquivalence.functor W E).map (NatTrans.mk fun X => NatTrans.app τ (L.obj X.as.obj)))
      x✝ =
    NatTrans.app ((whiskeringLeftFunctor L W E).map τ) x✝
[PROOFSTEP]
rfl
[GOAL]
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ X✝)).obj =
    ((whiskeringLeftFunctor L W E).obj X✝).obj
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ Y✝)).obj =
    ((whiskeringLeftFunctor L W E).obj Y✝).obj
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ X✝)).obj =
    ((whiskeringLeftFunctor L W E).obj X✝).obj
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ X✝)).obj =
    ((whiskeringLeftFunctor L W E).obj X✝).obj
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ Y✝)).obj =
    ((whiskeringLeftFunctor L W E).obj Y✝).obj
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ Y✝)).obj =
    ((whiskeringLeftFunctor L W E).obj Y✝).obj
[PROOFSTEP]
all_goals
  change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ _ = L ⋙ _
  rw [Construction.fac]
[GOAL]
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ X✝)).obj =
    ((whiskeringLeftFunctor L W E).obj X✝).obj
[PROOFSTEP]
change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ _ = L ⋙ _
[GOAL]
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ (MorphismProperty.Q W ⋙ Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)) ⋙ X✝ = L ⋙ X✝
[PROOFSTEP]
rw [Construction.fac]
[GOAL]
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ ((Construction.WhiskeringLeftEquivalence.functor W E).obj
        (Construction.lift L (_ : MorphismProperty.IsInvertedBy W L) ⋙ Y✝)).obj =
    ((whiskeringLeftFunctor L W E).obj Y✝).obj
[PROOFSTEP]
change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ _ = L ⋙ _
[GOAL]
case h.h.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.21739, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.21788, u_3} E
inst✝ : Functor.IsLocalization L W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ (MorphismProperty.Q W ⋙ Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)) ⋙ Y✝ = L ⋙ Y✝
[PROOFSTEP]
rw [Construction.fac]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.44449, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.44498, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Full (whiskeringLeftFunctor' L W E)
[PROOFSTEP]
rw [whiskeringLeftFunctor'_eq]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.44449, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.44498, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Full (whiskeringLeftFunctor L W E ⋙ inducedFunctor FullSubcategory.obj)
[PROOFSTEP]
apply @Full.comp _ _ _ _ _ _ _ _ ?_ ?_
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.44449, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.44498, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Full (whiskeringLeftFunctor L W E)
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.44449, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.44498, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Full (inducedFunctor FullSubcategory.obj)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.44449, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.44498, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Full (inducedFunctor FullSubcategory.obj)
[PROOFSTEP]
apply InducedCategory.full
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.46456, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.46505, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Faithful (whiskeringLeftFunctor' L W E)
[PROOFSTEP]
rw [whiskeringLeftFunctor'_eq]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.46456, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.46505, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Faithful (whiskeringLeftFunctor L W E ⋙ inducedFunctor FullSubcategory.obj)
[PROOFSTEP]
apply @Faithful.comp _ _ _ _ _ _ _ _ ?_ ?_
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.46456, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.46505, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Faithful (whiskeringLeftFunctor L W E)
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.46456, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.46505, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Faithful (inducedFunctor FullSubcategory.obj)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{?u.46456, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.46505, u_3} E
inst✝ : Functor.IsLocalization L W
⊢ Faithful (inducedFunctor FullSubcategory.obj)
[PROOFSTEP]
apply InducedCategory.faithful
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_5, u_3} E
inst✝ : Functor.IsLocalization L W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), NatTrans.app τ (L.obj X) = NatTrans.app τ' (L.obj X)
⊢ τ = τ'
[PROOFSTEP]
haveI : CategoryTheory.EssSurj L := essSurj L W
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_5, u_3} E
inst✝ : Functor.IsLocalization L W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), NatTrans.app τ (L.obj X) = NatTrans.app τ' (L.obj X)
this : EssSurj L
⊢ τ = τ'
[PROOFSTEP]
ext Y
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_5, u_3} E
inst✝ : Functor.IsLocalization L W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), NatTrans.app τ (L.obj X) = NatTrans.app τ' (L.obj X)
this : EssSurj L
Y : D
⊢ NatTrans.app τ Y = NatTrans.app τ' Y
[PROOFSTEP]
rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_4, u_3} E
inst✝ : Functor.IsLocalization L W
F₁ F₂ F₃ : C ⥤ E
F₁' F₂' F₃' : D ⥤ E
h₁ : Lifting L W F₁ F₁'
h₂ : Lifting L W F₂ F₂'
h₃ : Lifting L W F₃ F₃'
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
X : C
⊢ NatTrans.app (liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ') (L.obj X) =
    NatTrans.app (liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ')) (L.obj X)
[PROOFSTEP]
simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_4, u_3} E
inst✝ : Functor.IsLocalization L W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ NatTrans.app (liftNatTrans L W F F F' F' (𝟙 F)) (L.obj X) = NatTrans.app (𝟙 F') (L.obj X)
[PROOFSTEP]
simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_4, u_3} E
inst✝ : Functor.IsLocalization L W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ 𝟙 ((L ⋙ F').obj X) = 𝟙 (F'.obj (L.obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.74813, u_3} E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
⊢ IsLocalization L₂ W
[PROOFSTEP]
have h := Localization.inverts L₁ W
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.74813, u_3} E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₁
⊢ IsLocalization L₂ W
[PROOFSTEP]
rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h 
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.74813, u_3} E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₂
⊢ IsLocalization L₂ W
[PROOFSTEP]
let F₁ := Localization.Construction.lift L₁ (Localization.inverts L₁ W)
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.74813, u_3} E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₂
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L₁ (_ : MorphismProperty.IsInvertedBy W L₁)
⊢ IsLocalization L₂ W
[PROOFSTEP]
let F₂ := Localization.Construction.lift L₂ h
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_1, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{?u.74813, u_3} E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₂
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L₁ (_ : MorphismProperty.IsInvertedBy W L₁)
F₂ : MorphismProperty.Localization W ⥤ D := Construction.lift L₂ h
⊢ IsLocalization L₂ W
[PROOFSTEP]
exact
  { inverts := h
    nonempty_isEquivalence := Nonempty.intro (IsEquivalence.ofIso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) inferInstance) }
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_1, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type u_3
inst✝² : Category.{?u.76231, u_3} E✝
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
⊢ IsLocalization L' W
[PROOFSTEP]
have h : W.IsInvertedBy L' := by
  rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
  exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_1, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type u_3
inst✝² : Category.{?u.76231, u_3} E✝
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
⊢ MorphismProperty.IsInvertedBy W L'
[PROOFSTEP]
rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_1, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type u_3
inst✝² : Category.{?u.76231, u_3} E✝
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
⊢ MorphismProperty.IsInvertedBy W (L ⋙ eq.functor)
[PROOFSTEP]
exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_1, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type u_3
inst✝² : Category.{?u.76231, u_3} E✝
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
⊢ IsLocalization L' W
[PROOFSTEP]
let F₁ := Localization.Construction.lift L (Localization.inverts L W)
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_1, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type u_3
inst✝² : Category.{?u.76231, u_3} E✝
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
⊢ IsLocalization L' W
[PROOFSTEP]
let F₂ := Localization.Construction.lift L' h
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_1, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type u_3
inst✝² : Category.{?u.76231, u_3} E✝
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
F₂ : MorphismProperty.Localization W ⥤ E := Construction.lift L' h
⊢ IsLocalization L' W
[PROOFSTEP]
let e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' _ _ e
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_1, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type u_3
inst✝² : Category.{?u.76231, u_3} E✝
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
F₂ : MorphismProperty.Localization W ⥤ E := Construction.lift L' h
e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso (MorphismProperty.Q W) W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e
⊢ IsLocalization L' W
[PROOFSTEP]
exact
  { inverts := h
    nonempty_isEquivalence := Nonempty.intro (IsEquivalence.ofIso e' inferInstance) }
