Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

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