awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h :
  Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk (iResolutionObj X ≫ f))
    (RightHomotopyClass.mk (iResolutionObj X ≫ g))
⊢ Eq (α :=
    RightHomotopyClass (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
      (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)))
    (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
    (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))

Tactic:
exact (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
    (f := iResolutionObj X) (Z := Y)).1 h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ RightHomotopyRel (iResolutionObj X ≫ resolutionMap (𝟙 X))
    (iResolutionObj X ≫
      𝟙 (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X))))

Tactic:
simpa using .refl _
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} X)))
      (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} X))))
    (CategoryTheory.Functor.map toHoCat (homMk (resolutionMap (𝟙 X))))
    (CategoryTheory.Functor.map toHoCat (𝟙 (mk (resolutionObj.{v_1, u_1} X))))

Tactic:
exact resolutionObj_hom_ext (by simpa using .refl _)

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj_hom_ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ RightHomotopyRel (Y := resolutionObj.{v_1, u_1} X₃) (iResolutionObj X₁ ≫ resolutionMap (f ≫ g))
    (iResolutionObj X₁ ≫
      CategoryStruct.comp (Y :=
        ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X₂)))
        (InducedCategory.Hom.hom (homMk (resolutionMap f))) (InducedCategory.Hom.hom (homMk (resolutionMap g))))

Tactic:
simpa using .refl _
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Eq (α :=
    Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} X₁)))
      (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} X₃))))
    (CategoryTheory.Functor.map toHoCat (homMk (resolutionMap (f ≫ g))))
    (CategoryTheory.Functor.map toHoCat
      (CategoryStruct.comp (Y := mk (resolutionObj.{v_1, u_1} X₂)) (homMk (resolutionMap f)) (homMk (resolutionMap g))))

Tactic:
exact resolutionObj_hom_ext (by simpa using .refl _)

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj_hom_ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : C
x_2 : x ⟶ x_1
h : weakEquivalences C x_2
⊢ MorphismProperty.inverseImage (D := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C)) resolution x_2

Tactic:
simpa only [MorphismProperty.inverseImage_iff, ← weakEquivalence_iff, HoCat.resolution,
      weakEquivalence_toHoCat_map_iff, weakEquivalence_resolutionMap_iff,
      weakEquivalence_homMk_iff] using h

Premises used: HomotopicalAlgebra.FibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.FibrantObject.HoCat.weakEquivalence_resolutionMap_iff, HomotopicalAlgebra.FibrantObject.weakEquivalence_homMk_iff, CategoryTheory.MorphismProperty.inverseImage_iff, HomotopicalAlgebra.FibrantObject.HoCat.resolution
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : FibrantObject.{v_1, u_1} C
f : x ⟶ x_1
h :
  Eq (α :=
    (Functor.obj toHoCat x).as (r := homRel C).obj (P := fibrantObjects C) ⟶
      ObjectProperty.FullSubcategory.obj (P := fibrantObjects C)
        (Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1)))
    (InducedCategory.Hom.hom (f ≫ { hom := iResolutionObj (Functor.obj ι x_1) }))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x))
        { hom := iResolutionObj (Functor.obj ι x) } (homMk (resolutionMap (CategoryTheory.Functor.map ι f)))))
⊢ Eq (α := x ⟶ mk (resolutionObj.{v_1, u_1} (Functor.obj ι x_1))) (f ≫ { hom := iResolutionObj (Functor.obj ι x_1) })
    (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x))
      { hom := iResolutionObj (Functor.obj ι x) } (homMk (resolutionMap (CategoryTheory.Functor.map ι f))))

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : FibrantObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq (α :=
    (Functor.obj toHoCat x).as (r := homRel C).obj (P := fibrantObjects C) ⟶
      ObjectProperty.FullSubcategory.obj (P := fibrantObjects C)
        (Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1)))
    (InducedCategory.Hom.hom (f ≫ { hom := iResolutionObj (Functor.obj ι x_1) }))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x))
        { hom := iResolutionObj (Functor.obj ι x) } (homMk (resolutionMap (CategoryTheory.Functor.map ι f)))))

Tactic:
(HoCat.resolutionMap_fac f.hom).symm

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap, HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac, HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, Classical.choose, HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj, CategoryTheory.InducedCategory.Hom.hom, Eq.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : FibrantObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq (α :=
    (Functor.obj toHoCat x).as (r := homRel C).obj (P := fibrantObjects C) ⟶
      ObjectProperty.FullSubcategory.obj (P := fibrantObjects C)
        (Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1)))
    (InducedCategory.Hom.hom (f ≫ { hom := iResolutionObj (Functor.obj ι x_1) }))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x))
        { hom := iResolutionObj (Functor.obj ι x) } (homMk (resolutionMap (CategoryTheory.Functor.map ι f)))))

Tactic:
exact (HoCat.resolutionMap_fac f.hom).symm

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac, CategoryTheory.InducedCategory.Hom.hom, Eq.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : FibrantObject.{v_1, u_1} C
dsimp :
  WeakEquivalence.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (X := Functor.obj toHoCat X) (Y :=
    Functor.obj HoCat.resolution (X.obj (P := fibrantObjects C)))
    (CategoryTheory.Functor.map toHoCat { hom := HoCat.iResolutionObj (X.obj (P := fibrantObjects C)) })
⊢ WeakEquivalence (NatTrans.app HoCat.ιCompResolutionNatTrans X)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : FibrantObject.{v_1, u_1} C
rw :
  WeakEquivalence.{v_1, u_1} (C := C) (X := X.obj (P := fibrantObjects C)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := fibrantObjects C)
      (mk (HoCat.resolutionObj.{v_1, u_1} (X.obj (P := fibrantObjects C)))))
    (InducedCategory.Hom.hom { hom := HoCat.iResolutionObj (X.obj (P := fibrantObjects C)) })
⊢ WeakEquivalence.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (X := Functor.obj toHoCat X) (Y :=
    Functor.obj HoCat.resolution (X.obj (P := fibrantObjects C)))
    (CategoryTheory.Functor.map toHoCat { hom := HoCat.iResolutionObj (X.obj (P := fibrantObjects C)) })

Tactic:
rw [weakEquivalence_toHoCat_map_iff, weakEquivalence_iff_of_objectProperty]

Premises used: HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, HomotopicalAlgebra.FibrantObject.weakEquivalence_toHoCat_map_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : FibrantObject.{v_1, u_1} C
⊢ WeakEquivalence.{v_1, u_1} (C := C) (X := X.obj (P := fibrantObjects C)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := fibrantObjects C)
      (mk (HoCat.resolutionObj.{v_1, u_1} (X.obj (P := fibrantObjects C)))))
    (InducedCategory.Hom.hom { hom := HoCat.iResolutionObj (X.obj (P := fibrantObjects C)) })

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
rw : ∀ (X : FibrantObject.{v_1, u_1} C), IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).app X)
⊢ IsIso (Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
X : FibrantObject.{v_1, u_1} C
x : weakEquivalences (HoCat.{v_1, u_1} C) (NatTrans.app HoCat.ιCompResolutionNatTrans X)
⊢ IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).app X)

Tactic:
apply Localization.inverts L (weakEquivalences _)

Premises used: CategoryTheory.Localization.inverts, HomotopicalAlgebra.weakEquivalences
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
X : FibrantObject.{v_1, u_1} C
x : WeakEquivalence (NatTrans.app HoCat.ιCompResolutionNatTrans X)
⊢ weakEquivalences (HoCat.{v_1, u_1} C) (NatTrans.app HoCat.ιCompResolutionNatTrans X)

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
X : FibrantObject.{v_1, u_1} C
⊢ WeakEquivalence (NatTrans.app HoCat.ιCompResolutionNatTrans X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
x x_1 : C
f : x ⟶ x_1
⊢ L.map f ≫ L.map (iResolutionObj x_1) =
    L.map (iResolutionObj x) ≫ (Functor.comp (D := HoCat.{v_1, u_1} C) resolution (toLocalization L)).map f

Tactic:
simpa only [Functor.map_comp] using L.congr_map (HoCat.resolutionMap_fac f).symm

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, Eq.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
rw :
  ∀ (X : C),
    IsIso (Y := (Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)).obj X)
      (NatTrans.app (HoCat.resolutionCompToLocalizationNatTrans L) X)
⊢ IsIso (Y := Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (HoCat.resolutionCompToLocalizationNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
X : C
x :
  weakEquivalences.{v_1, u_1} C (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.iResolutionObj X)
⊢ IsIso (Y := (Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)).obj X)
    (NatTrans.app (HoCat.resolutionCompToLocalizationNatTrans L) X)

Tactic:
apply Localization.inverts L (weakEquivalences _)

Premises used: CategoryTheory.Localization.inverts, HomotopicalAlgebra.weakEquivalences
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
X : C
x :
  WeakEquivalence.{v_1, u_1} (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.iResolutionObj X)
⊢ weakEquivalences.{v_1, u_1} C (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.iResolutionObj X)

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
X : C
⊢ WeakEquivalence.{v_1, u_1} (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.iResolutionObj X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ LE.le (α := MorphismProperty.{v_1, u_1} (FibrantObject.{v_1, u_1} C)) (weakEquivalences (FibrantObject.{v_1, u_1} C))
    (weakEquivalences (FibrantObject.{v_1, u_1} C))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hfib : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lfibπ : HoCat.{v_1, u_1} C ⥤ Hfib := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lfib : FibrantObject.{v_1, u_1} C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hfib ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lfibπ F)
G : H ⥤ Hfib :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lfibπ G
have :
  ∀
    (this :
      Localization.Lifting L (weakEquivalences C)
        (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) (G ⋙ F)),
    LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
      weakEquivalences C) (localizerMorphism C)
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
have : Localization.Lifting L (weakEquivalences C)
      (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eG.symm _ ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eF'.symm⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hfib : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lfibπ : HoCat.{v_1, u_1} C ⥤ Hfib := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lfib : FibrantObject.{v_1, u_1} C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hfib ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lfibπ F)
G : H ⥤ Hfib :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lfibπ G
this :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
have :
  ∀
    (this :
      Localization.Lifting Lfib (weakEquivalences (FibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G)),
    LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
      weakEquivalences C) (localizerMorphism C)
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
have : Localization.Lifting Lfib (weakEquivalences (FibrantObject C))
        (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eF.symm G ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eG.symm⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hfib : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lfibπ : HoCat.{v_1, u_1} C ⥤ Hfib := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lfib : FibrantObject.{v_1, u_1} C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hfib ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lfibπ F)
G : H ⥤ Hfib :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lfibπ G
this_1 :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
this : Localization.Lifting Lfib (weakEquivalences (FibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G)
E : Hfib ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lfib (weakEquivalences (FibrantObject.{v_1, u_1} C)) Lfib (ι ⋙ HoCat.resolution ⋙ Lfibπ)
      (𝟭 Hfib) (F ⋙ G)
      (asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lfibπ) ≪≫ associator ι HoCat.resolution Lfibπ))
    (Localization.liftNatIso L (weakEquivalences C)
      (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) L (G ⋙ F) (𝟭 H)
      (Iso.symm (asIso (HoCat.resolutionCompToLocalizationNatTrans L))))
⊢ F.IsEquivalence

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