[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) }


[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
y : T
hy : y ∈ Y
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
[PROOFSTEP]
rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
[PROOFSTEP]
refine' ⟨U ⊓ Y, homOfLE inf_le_right, _, hU, hy⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ (Sieve.pullback f S).arrows (homOfLE (_ : U ⊓ Y ≤ Y))
[PROOFSTEP]
apply S.downward_closed hg (homOfLE inf_le_left)
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) Y
x : T
hx : x ∈ X
⊢ ∃ U f, R.arrows f ∧ x ∈ U
[PROOFSTEP]
rcases hS x hx with ⟨U, f, hf, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
⊢ ∃ U f, R.arrows f ∧ x ∈ U
[PROOFSTEP]
rcases hR hf _ hU with ⟨V, g, hg, hV⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : (Sieve.pullback f R).arrows g
hV : x ∈ V
⊢ ∃ U f, R.arrows f ∧ x ∈ U
[PROOFSTEP]
exact ⟨_, g ≫ f, hg, hV⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
⊢ ∃ U f_1, Presieve.pullbackArrows f S f_1 ∧ x ∈ U
[PROOFSTEP]
rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ ∃ U f_1, Presieve.pullbackArrows f S f_1 ∧ x ∈ U
[PROOFSTEP]
refine' ⟨_, _, Presieve.pullbackArrows.mk _ _ hg, _⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ x ∈ pullback g f
[PROOFSTEP]
have : U ⊓ Y ≤ pullback g f
[GOAL]
case this
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ U ⊓ Y ≤ pullback g f
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
this : U ⊓ Y ≤ pullback g f
⊢ x ∈ pullback g f
[PROOFSTEP]
refine' leOfHom (pullback.lift (homOfLE inf_le_left) (homOfLE inf_le_right) rfl)
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
this : U ⊓ Y ≤ pullback g f
⊢ x ∈ pullback g f
[PROOFSTEP]
apply this ⟨hU, hx⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) Y
x : T
hx : x ∈ X
⊢ ∃ U f, Presieve.bind S Ti f ∧ x ∈ U
[PROOFSTEP]
rcases hS x hx with ⟨U, f, hf, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
⊢ ∃ U f, Presieve.bind S Ti f ∧ x ∈ U
[PROOFSTEP]
rcases hTi f hf x hU with ⟨V, g, hg, hV⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : Ti f hf g
hV : x ∈ V
⊢ ∃ U f, Presieve.bind S Ti f ∧ x ∈ U
[PROOFSTEP]
exact ⟨_, _, ⟨_, g, f, hf, hg, rfl⟩, hV⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) = pretopology T
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) ≤ pretopology T
[PROOFSTEP]
intro X R hR x hx
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) X
x : T
hx : x ∈ X
⊢ ∃ U f, R f ∧ x ∈ U
[PROOFSTEP]
rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩
[GOAL]
case a.intro.intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hU : x ∈ U
V : Opens T
g₁ : U ⟶ V
g₂ : V ⟶ X
hg₂ : R g₂
right✝ : g₁ ≫ g₂ = f
⊢ ∃ U f, R f ∧ x ∈ U
[PROOFSTEP]
exact ⟨V, g₂, hg₂, g₁.le hU⟩
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)
[PROOFSTEP]
intro X R hR x hx
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (pretopology T) X
x : T
hx : x ∈ X
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U
[PROOFSTEP]
rcases hR x hx with ⟨U, f, hf, hU⟩
[GOAL]
case a.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (pretopology T) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : R f
hU : x ∈ U
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U
[PROOFSTEP]
exact ⟨U, f, Sieve.le_generate R U hf, hU⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (pretopology T) = grothendieckTopology T
[PROOFSTEP]
rw [← pretopology_ofGrothendieck]
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) =
    grothendieckTopology T
[PROOFSTEP]
apply (Pretopology.gi (Opens T)).l_u_eq