awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
h₁ : homRel C (X := mk X) (Y := mk (resolutionObj.{v_1, u_1} Y)) (homMk f) (homMk g)
⊢ Eq (α :=
    Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj toHoCat (mk X))
      (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} Y))))
    (CategoryTheory.Functor.map toHoCat (homMk f)) (CategoryTheory.Functor.map toHoCat (homMk g))

Tactic:
apply toHoCat_map_eq

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
h₁ :
  LeftHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y)))
    (InducedCategory.Hom.hom (homMk f)) (InducedCategory.Hom.hom (homMk g))
⊢ RightHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y)))
    (InducedCategory.Hom.hom (homMk f)) (InducedCategory.Hom.hom (homMk g))

Tactic:
apply LeftHomotopyRel.rightHomotopyRel

Premises used: HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
h₁ :
  ∀
    (h :
      Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk (f ≫ pResolutionObj Y))
        (LeftHomotopyClass.mk (g ≫ pResolutionObj Y))),
    Eq (α :=
      LeftHomotopyClass (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X))
        (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y))))
      (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
      (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))
⊢ LeftHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y)))
    (InducedCategory.Hom.hom (homMk f)) (InducedCategory.Hom.hom (homMk g))

Tactic:
rw [← LeftHomotopyClass.mk_eq_mk_iff] at h ⊢

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h :
  Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk (f ≫ pResolutionObj Y))
    (LeftHomotopyClass.mk (g ≫ pResolutionObj Y))
⊢ Eq (α :=
    LeftHomotopyClass (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X))
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y))))
    (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
    (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))

Tactic:
(LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence
    (X := X) (g := pResolutionObj Y)).injective h

Premises used: HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence, HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj, Function.Bijective.injective, Classical.choose
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h :
  Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk (f ≫ pResolutionObj Y))
    (LeftHomotopyClass.mk (g ≫ pResolutionObj Y))
⊢ Eq (α :=
    LeftHomotopyClass (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X))
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y))))
    (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
    (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))

Tactic:
exact (LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence
    (X := X) (g := pResolutionObj Y)).injective h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ LeftHomotopyRel (resolutionMap (𝟙 X) ≫ pResolutionObj X)
    (𝟙 (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} X))) ≫
      pResolutionObj X)

Tactic:
simpa using .refl _
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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.CofibrantObject.HoCat.resolutionObj_hom_ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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₃
⊢ LeftHomotopyRel (X := resolutionObj.{v_1, u_1} X₁) (resolutionMap (f ≫ g) ≫ pResolutionObj X₃)
    (CategoryStruct.comp (Y := resolutionObj.{v_1, u_1} X₃)
      (CategoryStruct.comp (Y :=
          ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} X₂)))
          (InducedCategory.Hom.hom (homMk (resolutionMap f))) (InducedCategory.Hom.hom (homMk (resolutionMap g))) :
        ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} X₁)) ⟶
          ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} X₃)))
      (pResolutionObj X₃))

Tactic:
simpa using .refl _
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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.CofibrantObject.HoCat.resolutionObj_hom_ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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.CofibrantObject.HoCat.weakEquivalence_resolutionMap_iff, HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.CofibrantObject.HoCat.resolution, CategoryTheory.MorphismProperty.inverseImage_iff, HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.CofibrantObject.weakEquivalence_homMk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : CofibrantObject.{v_1, u_1} C
f : x ⟶ x_1
h :
  Eq (α :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
        (Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x)) ⟶
      (Functor.obj toHoCat x_1).as (r := homRel C).obj (P := cofibrantObjects C))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1))
        (homMk (resolutionMap (CategoryTheory.Functor.map ι f))) { hom := pResolutionObj (Functor.obj ι x_1) }))
    (InducedCategory.Hom.hom ({ hom := pResolutionObj (Functor.obj ι x) } ≫ f))
⊢ Eq (α := mk (resolutionObj.{v_1, u_1} (Functor.obj ι x)) ⟶ x_1)
    (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1))
      (homMk (resolutionMap (CategoryTheory.Functor.map ι f))) { hom := pResolutionObj (Functor.obj ι x_1) })
    ({ hom := pResolutionObj (Functor.obj ι x) } ≫ f)

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

Tactic:
HoCat.resolutionMap_fac f.hom

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

Tactic:
exact HoCat.resolutionMap_fac f.hom

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : CofibrantObject.{v_1, u_1} C
dsimp :
  WeakEquivalence.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (X :=
    Functor.obj HoCat.resolution (X.obj (P := cofibrantObjects C))) (Y := Functor.obj toHoCat X)
    (CategoryTheory.Functor.map toHoCat { hom := HoCat.pResolutionObj (X.obj (P := cofibrantObjects C)) } :
      Functor.obj toHoCat (mk (HoCat.resolutionObj.{v_1, u_1} (X.obj (P := cofibrantObjects C)))) ⟶
        Functor.obj toHoCat X)
⊢ WeakEquivalence (NatTrans.app HoCat.ιCompResolutionNatTrans X)

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

Tactic:
rw [weakEquivalence_toHoCat_map_iff, weakEquivalence_iff_of_objectProperty]

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

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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 : CofibrantObject.{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.CofibrantObjectHomotopy
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 : CofibrantObject.{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.CofibrantObjectHomotopy
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 : CofibrantObject.{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.CofibrantObjectHomotopy
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 : CofibrantObject.{v_1, u_1} C
⊢ WeakEquivalence (NatTrans.app HoCat.ιCompResolutionNatTrans X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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
⊢ (Functor.comp (D := HoCat.{v_1, u_1} C) resolution (toLocalization L)).map f ≫ L.map (pResolutionObj x_1) =
    L.map (pResolutionObj x) ≫ L.map f

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

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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 (X := (Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)).obj X)
      (NatTrans.app (HoCat.resolutionCompToLocalizationNatTrans L) X)
⊢ IsIso (X := 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.CofibrantObjectHomotopy
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 (X :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.pResolutionObj X)
⊢ IsIso (X := (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.CofibrantObjectHomotopy
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} (X :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.pResolutionObj X)
⊢ weakEquivalences.{v_1, u_1} C (X :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.pResolutionObj X)

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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} (X :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.pResolutionObj X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
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} (CofibrantObject.{v_1, u_1} C))
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) (weakEquivalences (CofibrantObject.{v_1, u_1} C))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ 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 (CofibrantObject.{v_1, u_1} C)) (W₂ :=
      weakEquivalences C) (localizerMorphism C)
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{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⟩