awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : C
w : IsCofibrant.{v, u} X
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X))))
      (Functor.obj toHoCat
        (Functor.obj BifibrantObject.ιCofibrantObject
          (bifibrantResolutionObj (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk X)))))))
    (CategoryTheory.Functor.map toHoCat
        (iBifibrantResolutionObj (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))) ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat (mk X)))))
    (CategoryTheory.Functor.map toHoCat
        (iBifibrantResolutionObj (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))) ≫
      CategoryTheory.Functor.map toHoCat
        (homMk
          (InducedCategory.Hom.hom
            (iBifibrantResolutionObj
              (mk (ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (bifibrantResolutionObj (mk X))))))))

Tactic:
apply bifibrantResolutionMap_fac'

Premises used: HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.HoCat.{v, u} C
obtain :
  ∀ (X : BifibrantObject.{v, u} C),
    NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X)) ≫
        CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
          (NatTrans.app (Iso.hom adjCounitIso) (Functor.obj BifibrantObject.toHoCat X)) =
      𝟙 (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X))
⊢ NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject X) ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject (NatTrans.app (Iso.hom adjCounitIso) X) =
    𝟙 (Functor.obj BifibrantObject.HoCat.ιCofibrantObject X)

Tactic:
obtain ⟨X, rfl⟩ := BifibrantObject.toHoCat_obj_surjective X

Premises used: HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.{v, u} C
rw :
  NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X)) =
    inv
      (CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.hom adjCounitIso) (Functor.obj BifibrantObject.toHoCat X)))
⊢ NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X)) ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.hom adjCounitIso) (Functor.obj BifibrantObject.toHoCat X)) =
    𝟙 (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X))

Tactic:
rw [comp_hom_eq_id]

Premises used: CategoryTheory.comp_hom_eq_id
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.{v, u} C
push :
  NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X)) =
    CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
      (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj BifibrantObject.toHoCat X))
⊢ NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X)) =
    inv
      (CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.hom adjCounitIso) (Functor.obj BifibrantObject.toHoCat X)))

Tactic:
push inv

Premises used: CategoryTheory.inv
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.{v, u} C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X)) =
    CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
      (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj BifibrantObject.toHoCat X))
⊢ NatTrans.app adjUnit (Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X)) =
    CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
      (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj BifibrantObject.toHoCat X))

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ IsIso (C := CategoryTheory.Functor.{v, v, u, u} (BifibrantObject.HoCat.{v, u} C) (BifibrantObject.HoCat.{v, u} C))
    (Iso.hom HoCat.adjCounitIso)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ Functor.Full.{v, v, u, u} (C := BifibrantObject.HoCat.{v, u} C) BifibrantObject.HoCat.ιCofibrantObject

Tactic:
HoCat.adj.fullyFaithfulROfIsIsoCounit.full

Premises used: CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit, CategoryTheory.Functor.FullyFaithful.full, HomotopicalAlgebra.CofibrantObject.HoCat.adj
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ Functor.Faithful.{v, v, u, u} (C := BifibrantObject.HoCat.{v, u} C) BifibrantObject.HoCat.ιCofibrantObject

Tactic:
HoCat.adj.fullyFaithfulROfIsIsoCounit.faithful

Premises used: CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit, CategoryTheory.Functor.FullyFaithful.faithful, HomotopicalAlgebra.CofibrantObject.HoCat.adj
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : HoCat.{v, u} C
obtain :
  ∀ (X : CofibrantObject.{v, u} C), WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) (Functor.obj toHoCat X))
⊢ WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) X)

Tactic:
obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : CofibrantObject.{v, u} C
dsimp : WeakEquivalence (NatTrans.app HoCat.adjUnit (Functor.obj toHoCat X))
⊢ WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) (Functor.obj toHoCat X))

Tactic:
dsimp [HoCat.adj]

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.adj
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : CofibrantObject.{v, u} C
⊢ WeakEquivalence (NatTrans.app HoCat.adjUnit (Functor.obj toHoCat X))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : HoCat.{v, u} C
f : X ⟶ Y
hf : weakEquivalences (HoCat.{v, u} C) f
obtain :
  ∀ (X : CofibrantObject.{v, u} C) (f : Functor.obj toHoCat X ⟶ Y) (hf : weakEquivalences (HoCat.{v, u} C) f),
    IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
      (CategoryTheory.Functor.map HoCat.bifibrantResolution f)
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution X) (CategoryTheory.Functor.map HoCat.bifibrantResolution f)

Tactic:
obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
Y : HoCat.{v, u} C
X : CofibrantObject.{v, u} C
f : Functor.obj toHoCat X ⟶ Y
hf : weakEquivalences (HoCat.{v, u} C) f
obtain :
  ∀ (Y : CofibrantObject.{v, u} C) (f : Functor.obj toHoCat X ⟶ Functor.obj toHoCat Y)
    (hf : weakEquivalences (HoCat.{v, u} C) f),
    IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
      (CategoryTheory.Functor.map HoCat.bifibrantResolution f)
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
    (CategoryTheory.Functor.map HoCat.bifibrantResolution f)

Tactic:
obtain ⟨Y, rfl⟩ := toHoCat_obj_surjective Y

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : Functor.obj toHoCat X ⟶ Functor.obj toHoCat Y
hf : weakEquivalences (HoCat.{v, u} C) f
obtain :
  ∀ (f : X ⟶ Y)
    (hf : weakEquivalences (HoCat.{v, u} C) (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f)),
    IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
      (CategoryTheory.Functor.map HoCat.bifibrantResolution (CategoryTheory.Functor.map toHoCat f))
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
    (CategoryTheory.Functor.map HoCat.bifibrantResolution f)

Tactic:
obtain ⟨f, rfl⟩ := toHoCat.map_surjective f

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : weakEquivalences (HoCat.{v, u} C) (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f)
⊢ WeakEquivalence f

Tactic:
rw [← weakEquivalence_iff, weakEquivalence_toHoCat_map_iff] at hf

Premises used: HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
rw :
  IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X)) (Y :=
    Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat Y))
    (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap f) :
      Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶
        Functor.obj BifibrantObject.toHoCat Y.bifibrantResolutionObj)
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
    (CategoryTheory.Functor.map HoCat.bifibrantResolution (CategoryTheory.Functor.map toHoCat f))

Tactic:
rw [HoCat.bifibrantResolution_map]

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
x : weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X)) (Y :=
    Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat Y))
    (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap f) :
      Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶
        Functor.obj BifibrantObject.toHoCat Y.bifibrantResolutionObj)

Tactic:
apply Localization.inverts _ (weakEquivalences _)

Premises used: CategoryTheory.Localization.inverts, HomotopicalAlgebra.weakEquivalences
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
x : WeakEquivalence (bifibrantResolutionMap f)
⊢ weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : HoCat.{v, u} C
rw : WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) X)
⊢ weakEquivalences (HoCat.{v, u} C) (NatTrans.app (Adjunction.unit HoCat.adj) X)

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : HoCat.{v, u} C
dsimp : WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) X)
⊢ WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) X)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : HoCat.{v, u} C
⊢ WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ LE.le (α := MorphismProperty.{v, u} (BifibrantObject.{v, u} C)) (weakEquivalences (BifibrantObject.{v, u} C))
    (weakEquivalences (BifibrantObject.{v, u} C))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (BifibrantObject.{v, u} C)) (W₂ :=
    weakEquivalences (CofibrantObject.{v, u} C)) (ιCofibrantObjectLocalizerMorphism C)

Tactic:
let : CatCommSq (ιCofibrantObjectLocalizerMorphism C).functor toHoCat
      (CofibrantObject.toHoCat ⋙ CofibrantObject.HoCat.bifibrantResolution) (𝟭 _) :=
    ⟨(associator _ _ _).symm ≪≫
      isoWhiskerRight toHoCatCompιCofibrantObject.symm _ ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ (asIso CofibrantObject.HoCat.adj.counit)⟩
  LocalizerMorphism.IsLocalizedEquivalence.mk'
    (ιCofibrantObjectLocalizerMorphism C) BifibrantObject.toHoCat
    (CofibrantObject.toHoCat ⋙ CofibrantObject.HoCat.bifibrantResolution) (𝟭 _)

Premises used: HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject, HomotopicalAlgebra.BifibrantObject.toHoCatCompιCofibrantObject, CategoryTheory.Functor.comp, HomotopicalAlgebra.BifibrantObject.toHoCat, CategoryTheory.Functor.id, CategoryTheory.Functor.associator, CategoryTheory.CatCommSq.mk, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Adjunction.counit, HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.toHoCat, CategoryTheory.Iso.trans, HomotopicalAlgebra.CofibrantObject.HoCat.adj, CategoryTheory.Iso.symm, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk', HomotopicalAlgebra.BifibrantObject.HoCat, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{u_2, u_1} D
L : CategoryTheory.Functor.{v, u_2, u, u_1} (CofibrantObject.{v, u} C) D
inst_3 : L.IsLocalization (weakEquivalences (CofibrantObject.{v, u} C))
⊢ IsLocalization (C := BifibrantObject.{v, u} C) (ιCofibrantObject ⋙ L) (weakEquivalences (BifibrantObject.{v, u} C))

Tactic:
inferInstanceAs (((ιCofibrantObjectLocalizerMorphism C).functor ⋙ L).IsLocalization _)

Premises used: _private.0.HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompCofibrantObjectιCofibrantObjectWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (BifibrantObject.{v, u} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
inferInstanceAs ((ιCofibrantObjectLocalizerMorphism C).comp
    (CofibrantObject.localizerMorphism C)).IsLocalizedEquivalence

Premises used: _private.0.HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
L : CategoryTheory.Functor.{v, v_1, u, u_1} C D
inst_3 : L.IsLocalization (weakEquivalences C)
⊢ IsLocalization (C := BifibrantObject.{v, u} C) (ι ⋙ L) (weakEquivalences (BifibrantObject.{v, u} C))

Tactic:
inferInstanceAs (((localizerMorphism C).functor ⋙ L).IsLocalization _)

Premises used: _private.0.HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompιWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (BifibrantObject.{v, u} C)) (W₂ :=
    weakEquivalences (FibrantObject.{v, u} C)) (ιFibrantObjectLocalizerMorphism C)

Tactic:
let L := FibrantObject.ι ⋙ (weakEquivalences C).Q
  have : ((ιFibrantObjectLocalizerMorphism C).functor ⋙ L).IsLocalization
    (weakEquivalences _) :=
    inferInstanceAs ((ι ⋙ (weakEquivalences C).Q).IsLocalization (weakEquivalences _))
  LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization _ L

Premises used: HomotopicalAlgebra.FibrantObject.ι, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization, HomotopicalAlgebra.weakEquivalences, _private.0.HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceFibrantObjectWeakEquivalencesιFibrantObjectLocalizerMorphism._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{u_2, u_1} D
L : CategoryTheory.Functor.{v, u_2, u, u_1} (FibrantObject.{v, u} C) D
inst_3 : L.IsLocalization (weakEquivalences (FibrantObject.{v, u} C))
⊢ IsLocalization (C := BifibrantObject.{v, u} C) (ιFibrantObject ⋙ L) (weakEquivalences (BifibrantObject.{v, u} C))

Tactic:
inferInstanceAs (((ιFibrantObjectLocalizerMorphism C).functor ⋙ L).IsLocalization _)

Premises used: _private.0.HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompFibrantObjectιFibrantObjectWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
L : CategoryTheory.Functor.{v, v_1, u, u_1} C D
inst_3 : L.IsLocalization (weakEquivalences C)
inst_4 : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v_1, u_1} D

Tactic:
locallySmall_of_faithful ((BifibrantObject.localizerMorphism C).localizedFunctor
    BifibrantObject.toHoCat L).inv

Premises used: HomotopicalAlgebra.BifibrantObject.localizerMorphism, HomotopicalAlgebra.BifibrantObject.toHoCat, CategoryTheory.locallySmall_of_faithful, CategoryTheory.Functor.inv, CategoryTheory.LocalizerMorphism.localizedFunctor
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : CofibrantBrownFactorization f
inst_2 : WeakEquivalence f
⊢ WeakEquivalence (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
weakEquivalence_of_postcomp_of_fac h.fac

Premises used: HomotopicalAlgebra.CofibrantBrownFactorization.toMapFactorizationData, CategoryTheory.MorphismProperty.MapFactorizationData.fac, HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : CofibrantBrownFactorization f
⊢ WeakEquivalence h.s

Tactic:
weakEquivalence_of_postcomp_of_fac h.s_p

Premises used: HomotopicalAlgebra.CofibrantBrownFactorization.s_p, HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
rw : Cofibration (coprod.inl ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ cofibrations C (coprod.inl ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
rw [← cofibration_iff]

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
⊢ Cofibration (coprod.inl ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
rw :
  Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ∧
    WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ trivialFibrations C (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
rw [mem_trivialFibrations_iff]

Premises used: HomotopicalAlgebra.mem_trivialFibrations_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
left : Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
right : WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ∧
    WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
⊢ Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
infer_instance