C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₁
⊢ IsLocalization L₂ W
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
⊢ IsLocalization L₂ W
have h := Localization.inverts L₁ W
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₂
⊢ IsLocalization L₂ W
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₁
⊢ IsLocalization L₂ W
rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category 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
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category E
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : IsLocalization L₁ W
h : MorphismProperty.IsInvertedBy W L₂
⊢ IsLocalization L₂ W
let F₁ := Localization.Construction.lift L₁ (Localization.inverts L₁ W)
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category 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
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category 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
let F₂ := Localization.Construction.lift L₂ h
no goals
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type ?u.76257
inst✝¹ : Category 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
exact
  { inverts := h
    nonempty_isEquivalence :=
      Nonempty.intro (IsEquivalence.ofIso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) inferInstance) }