-- Mathlib/CategoryTheory/Localization/Predicate.lean
theorem of_equivalence_target {E : Type*} [Category E] (L' : C ⥤ E) (eq : D ≌ E)
    [L.IsLocalization W] (e : L ⋙ eq.functor ≅ L') : L'.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
⊢ L'.IsLocalization W

Tactic:
let F₁ := Localization.Construction.lift L (Localization.inverts L W)

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift L ⋯
⊢ L'.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift L ⋯
⊢ L'.IsLocalization W

Tactic:
let F₂ := Localization.Construction.lift L' h

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift L ⋯
F₂ : W.Localization ⥤ E := Construction.lift L' h
⊢ L'.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy L'

Tactic:
rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy (L ⋙ eq.functor)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ L'.IsLocalization W

Tactic:
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

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
⊢ L'.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift L ⋯
F₂ : W.Localization ⥤ E := Construction.lift L' h
e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e
⊢ L'.IsLocalization W

Tactic:
exact
  { inverts := h
    isEquivalence := Functor.isEquivalence_of_iso e' }

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy (L ⋙ eq.functor)

Tactic:
exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift L ⋯
F₂ : W.Localization ⥤ E := Construction.lift L' h
⊢ L'.IsLocalization W

Tactic:
let e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' _ _ e

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_7, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift L ⋯
F₂ : W.Localization ⥤ E := Construction.lift L' h
e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e
⊢ L'.IsLocalization W