Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lfibπ F)
G : H ⥤ Hfib := (HoCat.localizerMorphismResolution C).localizedFunctor L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lfibπ G
this✝ : Localization.Lifting L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F)
this : Localization.Lifting Lfib (weakEquivalences (FibrantObject C)) (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G)
E : Hfib ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lfib (weakEquivalences (FibrantObject C)) Lfib (ι ⋙ HoCat.resolution ⋙ Lfibπ) (𝟭 Hfib)
      (F ⋙ G) (asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lfibπ) ≪≫ ι.associator HoCat.resolution Lfibπ))
    (Localization.liftNatIso L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) L (G ⋙ F) (𝟭 H)
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)).symm)
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
have : F.IsEquivalence := E.isEquivalence_functor

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lfibπ F)
G : H ⥤ Hfib := (HoCat.localizerMorphismResolution C).localizedFunctor L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lfibπ G
this✝¹ : Localization.Lifting L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F)
this✝ : Localization.Lifting Lfib (weakEquivalences (FibrantObject C)) (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G)
E : Hfib ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lfib (weakEquivalences (FibrantObject C)) Lfib (ι ⋙ HoCat.resolution ⋙ Lfibπ) (𝟭 Hfib)
      (F ⋙ G) (asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lfibπ) ≪≫ ι.associator HoCat.resolution Lfibπ))
    (Localization.liftNatIso L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) L (G ⋙ F) (𝟭 H)
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)).symm)
this : F.IsEquivalence
⊢ (localizerMorphism C).IsLocalizedEquivalence