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₁ X₂ : BifibrantObject.{v, u} C
f : X₁ ⟶ X₂
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (cofibrantObjects C))
        (ObjectProperty.ι (cofibrantObjects C)) (mk (X₁.obj (P := bifibrantObjects C))) ⟶
      Functor.obj.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (cofibrantObjects C))
        (ObjectProperty.ι (cofibrantObjects C))
        (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C))))))
    (CategoryTheory.Functor.map (ObjectProperty.ι (cofibrantObjects C))
      (homMk f.hom ≫ iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C)))))
    (CategoryTheory.Functor.map (ObjectProperty.ι (cofibrantObjects C))
      (iBifibrantResolutionObj (mk (X₁.obj (P := bifibrantObjects C))) ≫
        homMk (InducedCategory.Hom.hom (bifibrantResolutionMap (homMk f.hom)))))
h :
  f.hom ≫ InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C)))) =
    InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₁.obj (P := bifibrantObjects C)))) ≫
      (bifibrantResolutionMap (ObjectProperty.homMk (P := cofibrantObjects C) f.hom)).hom
⊢ Eq (α :=
    (Quotient.as (r := BifibrantObject.homRel C)
            (Functor.obj (Quotient.functor (BifibrantObject.homRel C) ⋙ 𝟭 (BifibrantObject.HoCat.{v, u} C)) X₁)).obj
        (P := bifibrantObjects C) ⟶
      (Functor.obj
                (Quotient.functor (BifibrantObject.homRel C) ⋙
                  BifibrantObject.HoCat.ιCofibrantObject ⋙ bifibrantResolution)
                X₂).as
            (r := BifibrantObject.homRel C).obj
        (P := bifibrantObjects C))
    (InducedCategory.Hom.hom
      (f ≫
        BifibrantObject.homMk
          (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C)))))))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        (Functor.obj
              (Quotient.functor (BifibrantObject.homRel C) ⋙
                BifibrantObject.HoCat.ιCofibrantObject ⋙ bifibrantResolution)
              X₁).as
          (r := BifibrantObject.homRel C))
        (BifibrantObject.homMk
          (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₁.obj (P := bifibrantObjects C))))))
        (bifibrantResolutionMap (CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject f))))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ : BifibrantObject.{v, u} C
f : X₁ ⟶ X₂
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (cofibrantObjects C))
        (ObjectProperty.ι (cofibrantObjects C)) (mk (X₁.obj (P := bifibrantObjects C))) ⟶
      Functor.obj.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (cofibrantObjects C))
        (ObjectProperty.ι (cofibrantObjects C))
        (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C))))))
    (CategoryTheory.Functor.map (ObjectProperty.ι (cofibrantObjects C))
      (homMk f.hom ≫ iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C)))))
    (CategoryTheory.Functor.map (ObjectProperty.ι (cofibrantObjects C))
      (iBifibrantResolutionObj (mk (X₁.obj (P := bifibrantObjects C))) ≫
        homMk (InducedCategory.Hom.hom (bifibrantResolutionMap (homMk f.hom)))))
⊢ f.hom ≫ InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C)))) =
    InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₁.obj (P := bifibrantObjects C)))) ≫
      (bifibrantResolutionMap (ObjectProperty.homMk (P := cofibrantObjects C) f.hom)).hom

Tactic:
this

Premises used: HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj, HomotopicalAlgebra.cofibrantObjects, Classical.choose, HomotopicalAlgebra.bifibrantObjects
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ : BifibrantObject.{v, u} C
f : X₁ ⟶ X₂
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (cofibrantObjects C))
        (ObjectProperty.ι (cofibrantObjects C)) (mk (X₁.obj (P := bifibrantObjects C))) ⟶
      Functor.obj.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (cofibrantObjects C))
        (ObjectProperty.ι (cofibrantObjects C))
        (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C))))))
    (CategoryTheory.Functor.map (ObjectProperty.ι (cofibrantObjects C))
      (homMk f.hom ≫ iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C)))))
    (CategoryTheory.Functor.map (ObjectProperty.ι (cofibrantObjects C))
      (iBifibrantResolutionObj (mk (X₁.obj (P := bifibrantObjects C))) ≫
        homMk (InducedCategory.Hom.hom (bifibrantResolutionMap (homMk f.hom)))))
⊢ f.hom ≫ InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C)))) =
    InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₁.obj (P := bifibrantObjects C)))) ≫
      (bifibrantResolutionMap (ObjectProperty.homMk (P := cofibrantObjects C) f.hom)).hom

Tactic:
exact this
-- 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
⊢ NatTrans.app adjCounit' (Functor.obj BifibrantObject.toHoCat X) =
    CategoryTheory.Functor.map BifibrantObject.toHoCat
      (BifibrantObject.homMk (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C))))))

Tactic:
rfl

Premises used: HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj, HomotopicalAlgebra.cofibrantObjects, Classical.choose, HomotopicalAlgebra.bifibrantObjects, rfl
-- 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), IsIso (NatTrans.app HoCat.adjCounit' (Functor.obj BifibrantObject.toHoCat X))
⊢ IsIso (NatTrans.app HoCat.adjCounit' 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 :
  IsIso.{v, u} (C := BifibrantObject.HoCat.{v, u} C) (X :=
    Functor.obj.{v, v, u, u} (𝟭 (BifibrantObject.HoCat.{v, u} C)) (Functor.obj BifibrantObject.toHoCat X)) (Y :=
    Functor.obj (BifibrantObject.HoCat.ιCofibrantObject ⋙ HoCat.bifibrantResolution)
      (Functor.obj BifibrantObject.toHoCat X))
    (CategoryTheory.Functor.map BifibrantObject.toHoCat
        (BifibrantObject.homMk
          (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))) :
      Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C)
        (Functor.obj BifibrantObject.toHoCat
          (BifibrantObject.mk
            (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (X.obj (P := bifibrantObjects C))))))
        (Functor.obj BifibrantObject.toHoCat
          (BifibrantObject.mk
            (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
              (Functor.obj BifibrantObject.ιCofibrantObject
                (bifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))))))
⊢ IsIso (NatTrans.app HoCat.adjCounit' (Functor.obj BifibrantObject.toHoCat X))

Tactic:
rw [HoCat.adjCounit'_app]

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app
-- 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
simp :
  WeakEquivalence.{v, u} (X := X.obj (P := bifibrantObjects C)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
      (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C))))))
    (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))
⊢ WeakEquivalence.{v, u} (C := BifibrantObject.{v, u} C) (X :=
    BifibrantObject.mk
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (X.obj (P := bifibrantObjects C)))))
    (Y :=
    BifibrantObject.mk
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
        (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))))
    (BifibrantObject.homMk (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C))))))

Tactic:
simp only [BifibrantObject.weakEquivalence_homMk_iff]

Premises used: HomotopicalAlgebra.BifibrantObject.weakEquivalence_homMk_iff
-- 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
⊢ WeakEquivalence.{v, u} (X := X.obj (P := bifibrantObjects C)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
      (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C))))))
    (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))

Tactic:
infer_instance
-- 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
⊢ WeakEquivalence.{v, u} (C := BifibrantObject.{v, u} C) (X :=
    BifibrantObject.mk
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (X.obj (P := bifibrantObjects C)))))
    (Y :=
    BifibrantObject.mk
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
        (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))))
    (BifibrantObject.homMk (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C))))))

Tactic:
have : WeakEquivalence (C := BifibrantObject C)
      (BifibrantObject.homMk ((mk X.obj).iBifibrantResolutionObj).hom) := by
    simp only [BifibrantObject.weakEquivalence_homMk_iff]
    infer_instance
-- 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
this :
  WeakEquivalence.{v, u} (C := BifibrantObject.{v, u} C) (X :=
    BifibrantObject.mk
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (X.obj (P := bifibrantObjects C)))))
    (Y :=
    BifibrantObject.mk
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
        (Functor.obj BifibrantObject.ιCofibrantObject (bifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))))
    (BifibrantObject.homMk (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C))))))
⊢ IsIso.{v, u} (C := BifibrantObject.HoCat.{v, u} C) (X :=
    Functor.obj.{v, v, u, u} (𝟭 (BifibrantObject.HoCat.{v, u} C)) (Functor.obj BifibrantObject.toHoCat X)) (Y :=
    Functor.obj (BifibrantObject.HoCat.ιCofibrantObject ⋙ HoCat.bifibrantResolution)
      (Functor.obj BifibrantObject.toHoCat X))
    (CategoryTheory.Functor.map BifibrantObject.toHoCat
        (BifibrantObject.homMk
          (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))) :
      Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C)
        (Functor.obj BifibrantObject.toHoCat
          (BifibrantObject.mk
            (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (X.obj (P := bifibrantObjects C))))))
        (Functor.obj BifibrantObject.toHoCat
          (BifibrantObject.mk
            (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
              (Functor.obj BifibrantObject.ιCofibrantObject
                (bifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C)))))))))

Tactic:
infer_instance
-- 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))
    HoCat.adjCounit'

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- 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
⊢ NatTrans.app (Iso.inv adjCounitIso) (Functor.obj BifibrantObject.toHoCat X) =
    CategoryTheory.Functor.map BifibrantObject.toHoCat
      (BifibrantObject.homMk (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X.obj (P := bifibrantObjects C))))))

Tactic:
rfl

Premises used: HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj, HomotopicalAlgebra.cofibrantObjects, Classical.choose, HomotopicalAlgebra.bifibrantObjects, rfl
-- 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),
    CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat X)) ≫
        NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat X)) =
      𝟙 (Functor.obj bifibrantResolution (Functor.obj toHoCat X))
⊢ CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit X) ≫
      NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution X) =
    𝟙 (Functor.obj bifibrantResolution 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
obtain :
  ∀ (X : C) (w : IsCofibrant.{v, u} X),
    Eq.{v + 1} (α :=
      Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))
        (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))
      (CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat (mk X))) ≫
        NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))
      (𝟙 (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))
⊢ CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat X)) ≫
      NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat X)) =
    𝟙 (Functor.obj bifibrantResolution (Functor.obj toHoCat X))

Tactic:
obtain ⟨X, _, rfl⟩ := CofibrantObject.mk_surjective X

Premises used: HomotopicalAlgebra.CofibrantObject.mk_surjective, rfl
-- 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
rw :
  Eq.{v + 1} (α :=
    Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))
      (Functor.obj bifibrantResolution
        (Functor.obj BifibrantObject.HoCat.ιCofibrantObject
          (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))))
    (CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat (mk X))))
    (inv (NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))
      (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))
    (CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat (mk X))) ≫
      NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))
    (𝟙 (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk 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 : C
w : IsCofibrant.{v, u} X
push :
  Eq.{v + 1} (α :=
    Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))
      (Functor.obj bifibrantResolution
        (Functor.obj BifibrantObject.HoCat.ιCofibrantObject
          (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))))
    (CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat (mk X))))
    (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))
      (Functor.obj bifibrantResolution
        (Functor.obj BifibrantObject.HoCat.ιCofibrantObject
          (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))))
    (CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat (mk X))))
    (inv (NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk 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 : C
w : IsCofibrant.{v, u} X
h :
  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 BifibrantObject.HoCat.ιCofibrantObject
        (Functor.obj bifibrantResolution
          (Functor.obj BifibrantObject.HoCat.ιCofibrantObject
            (Functor.obj bifibrantResolution (Functor.obj toHoCat (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 BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := BifibrantObject.HoCat.{v, u} C) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))
      (Functor.obj bifibrantResolution
        (Functor.obj BifibrantObject.HoCat.ιCofibrantObject
          (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))))
    (CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit (Functor.obj toHoCat (mk X))))
    (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X))))

Tactic:
apply bifibrantResolutionObj_hom_ext

Premises used: HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj_hom_ext
-- 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
h :
  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 BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj BifibrantObject.toHoCat (bifibrantResolutionObj (mk 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 BifibrantObject.HoCat.ιCofibrantObject
        (Functor.obj bifibrantResolution
          (Functor.obj BifibrantObject.HoCat.ιCofibrantObject
            (Functor.obj bifibrantResolution (Functor.obj toHoCat (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 BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj bifibrantResolution (Functor.obj toHoCat (mk X)))))

Tactic:
dsimp
-- 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
h :
  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))))))))
⊢ 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 BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj BifibrantObject.toHoCat (bifibrantResolutionObj (mk X)))))

Tactic:
simp only [HoCat.adjCounitIso_inv_app,
      BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, ObjectProperty.homMk_hom]

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, CategoryTheory.ObjectProperty.homMk_hom