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 : CofibrantObject.{v, u} C
Y : BifibrantObject.HoCat.{v, u} C
f g : Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Y
h :
  Eq (α := Functor.obj toHoCat X ⟶ Functor.obj BifibrantObject.HoCat.ιCofibrantObject Y)
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject f)
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject g)
obtain :
  ∀ (Y : BifibrantObject.{v, u} C)
    {f g : Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y}
    (h :
      Eq (α :=
        Functor.obj toHoCat X ⟶
          Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat Y))
        (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
          CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject f)
        (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
          CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject g)),
    f = g
⊢ f = g

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

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 : CofibrantObject.{v, u} C
Y : BifibrantObject.{v, u} C
f g : Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y
h :
  Eq (α :=
    Functor.obj toHoCat X ⟶ Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat Y))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject f)
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject g)
obtain :
  ∀ (f : X.bifibrantResolutionObj ⟶ Y)
    (h :
      Eq (α :=
        Functor.obj toHoCat X ⟶
          Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat Y))
        (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
          CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
            (CategoryTheory.Functor.map BifibrantObject.toHoCat f))
        (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
          CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject g)),
    CategoryTheory.Functor.map BifibrantObject.toHoCat f = g
⊢ f = g

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

Premises used: HomotopicalAlgebra.BifibrantObject.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 : CofibrantObject.{v, u} C
Y : BifibrantObject.{v, u} C
g : Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y
f : X.bifibrantResolutionObj ⟶ Y
h :
  Eq (α :=
    Functor.obj toHoCat X ⟶ Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat Y))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map BifibrantObject.toHoCat f))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject g)
obtain :
  ∀ (g : X.bifibrantResolutionObj ⟶ Y)
    (h :
      Eq (α :=
        Functor.obj toHoCat X ⟶
          Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat Y))
        (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
          CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
            (CategoryTheory.Functor.map BifibrantObject.toHoCat f))
        (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
          CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
            (CategoryTheory.Functor.map BifibrantObject.toHoCat g))),
    Eq (α := Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y)
      (CategoryTheory.Functor.map BifibrantObject.toHoCat f) (CategoryTheory.Functor.map BifibrantObject.toHoCat g)
⊢ CategoryTheory.Functor.map BifibrantObject.toHoCat f = g

Tactic:
obtain ⟨g, rfl⟩ := BifibrantObject.toHoCat.map_surjective g

Premises used: HomotopicalAlgebra.BifibrantObject.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 : CofibrantObject.{v, u} C
Y : BifibrantObject.{v, u} C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  Eq (α :=
    Functor.obj toHoCat X ⟶ Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat Y))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map BifibrantObject.toHoCat f))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map BifibrantObject.toHoCat g))
⊢ Eq (α := Functor.obj toHoCat X ⟶ Functor.obj toHoCat (Functor.obj BifibrantObject.ιCofibrantObject Y))
    (CategoryTheory.Functor.map toHoCat
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject f))
    (CategoryTheory.Functor.map toHoCat
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g))

Tactic:
change toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f) =
    toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g) at h

Premises used: CategoryTheory.Functor.map, HomotopicalAlgebra.CofibrantObject.toHoCat, CategoryTheory.CategoryStruct.comp, HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj, HomotopicalAlgebra.BifibrantObject.ιCofibrantObject
-- 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
Y : BifibrantObject.{v, u} C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  Eq (α := Functor.obj toHoCat X ⟶ Functor.obj toHoCat (Functor.obj BifibrantObject.ιCofibrantObject Y))
    (CategoryTheory.Functor.map toHoCat
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject f))
    (CategoryTheory.Functor.map toHoCat
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g))
⊢ Eq (α :=
    RightHomotopyClass (X.obj (P := cofibrantObjects C))
      ((Functor.obj BifibrantObject.ιCofibrantObject Y).obj (P := cofibrantObjects C)))
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject f).hom)
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g).hom)

Tactic:
rw [CofibrantObject.toHoCat_map_eq_iff,
    CofibrantObject.homRel_iff_rightHomotopyRel,
    ← RightHomotopyClass.mk_eq_mk_iff] at h

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff, HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel
-- 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
Y : BifibrantObject.{v, u} C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  Eq (α :=
    RightHomotopyClass (X.obj (P := cofibrantObjects C))
      ((Functor.obj BifibrantObject.ιCofibrantObject Y).obj (P := cofibrantObjects C)))
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject f).hom)
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g).hom)
rw :
  Eq (α :=
    RightHomotopyClass (X.bifibrantResolutionObj.obj (P := bifibrantObjects C)) (Y.obj (P := bifibrantObjects C)))
    (RightHomotopyClass.mk f.hom) (RightHomotopyClass.mk g.hom)
⊢ Eq (α := Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y)
    (CategoryTheory.Functor.map BifibrantObject.toHoCat f) (CategoryTheory.Functor.map BifibrantObject.toHoCat g)

Tactic:
rw [BifibrantObject.toHoCat_map_eq_iff,
    BifibrantObject.homRel_iff_rightHomotopyRel,
    ← RightHomotopyClass.mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff, HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel
-- 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
Y : BifibrantObject.{v, u} C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  Eq (α :=
    RightHomotopyClass (X.obj (P := cofibrantObjects C))
      ((Functor.obj BifibrantObject.ιCofibrantObject Y).obj (P := cofibrantObjects C)))
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject f).hom)
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g).hom)
a :
  Eq.{v + 1} (α := RightHomotopyClass (X.obj (P := cofibrantObjects C)) (Y.obj (P := bifibrantObjects C)))
    ((fun
          (g :
            RightHomotopyClass
              ((Functor.obj BifibrantObject.ιCofibrantObject X.bifibrantResolutionObj).obj (P := cofibrantObjects C))
              (Y.obj (P := bifibrantObjects C))) ↦
        g.precomp X.iBifibrantResolutionObj.hom)
      (RightHomotopyClass.mk f.hom))
    ((fun
          (g :
            RightHomotopyClass
              ((Functor.obj BifibrantObject.ιCofibrantObject X.bifibrantResolutionObj).obj (P := cofibrantObjects C))
              (Y.obj (P := bifibrantObjects C))) ↦
        g.precomp X.iBifibrantResolutionObj.hom)
      (RightHomotopyClass.mk g.hom))
⊢ Eq (α :=
    RightHomotopyClass (X.bifibrantResolutionObj.obj (P := bifibrantObjects C)) (Y.obj (P := bifibrantObjects C)))
    (RightHomotopyClass.mk f.hom) (RightHomotopyClass.mk g.hom)

Tactic:
apply (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
    _ (iBifibrantResolutionObj X).hom).1

Premises used: HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence, And.left, HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj, CategoryTheory.InducedCategory.Hom.hom
-- 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
Y : BifibrantObject.{v, u} C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  Eq (α :=
    RightHomotopyClass (X.obj (P := cofibrantObjects C))
      ((Functor.obj BifibrantObject.ιCofibrantObject Y).obj (P := cofibrantObjects C)))
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject f).hom)
    (RightHomotopyClass.mk
      (X.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g).hom)
⊢ Eq.{v + 1} (α := RightHomotopyClass (X.obj (P := cofibrantObjects C)) (Y.obj (P := bifibrantObjects C)))
    ((fun
          (g :
            RightHomotopyClass
              ((Functor.obj BifibrantObject.ιCofibrantObject X.bifibrantResolutionObj).obj (P := cofibrantObjects C))
              (Y.obj (P := bifibrantObjects C))) ↦
        g.precomp X.iBifibrantResolutionObj.hom)
      (RightHomotopyClass.mk f.hom))
    ((fun
          (g :
            RightHomotopyClass
              ((Functor.obj BifibrantObject.ιCofibrantObject X.bifibrantResolutionObj).obj (P := cofibrantObjects C))
              (Y.obj (P := bifibrantObjects C))) ↦
        g.precomp X.iBifibrantResolutionObj.hom)
      (RightHomotopyClass.mk g.hom))

Tactic:
simpa using h
-- 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
⊢ Eq (α :=
    Functor.obj toHoCat X ⟶
      Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap (𝟙 X))))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (𝟙 (Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj)))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ X₃ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Eq (α :=
    Functor.obj toHoCat X₁ ⟶
      Functor.obj BifibrantObject.HoCat.ιCofibrantObject
        (Functor.obj BifibrantObject.toHoCat X₃.bifibrantResolutionObj))
    (CategoryTheory.Functor.map toHoCat X₁.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap (f ≫ g))))
    (CategoryTheory.Functor.map toHoCat X₁.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap f) ≫
          CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap g)))

Tactic:
simp
-- 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 g : X ⟶ Y
h : homRel C f g
h₁ :
  Eq (α :=
    Functor.obj toHoCat X ⟶ Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj bifibrantResolution' Y))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map bifibrantResolution' f))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map bifibrantResolution' g))
⊢ Eq (α := Functor.obj bifibrantResolution' X ⟶ Functor.obj bifibrantResolution' Y)
    (CategoryTheory.Functor.map bifibrantResolution' f) (CategoryTheory.Functor.map bifibrantResolution' g)

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 Y : CofibrantObject.{v, u} C
f g : X ⟶ Y
h : homRel C f g
⊢ Eq (α :=
    Functor.obj toHoCat X ⟶ Functor.obj BifibrantObject.HoCat.ιCofibrantObject (Functor.obj bifibrantResolution' Y))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map bifibrantResolution' f))
    (CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj ≫
      CategoryTheory.Functor.map BifibrantObject.HoCat.ιCofibrantObject
        (CategoryTheory.Functor.map bifibrantResolution' g))

Tactic:
simpa [← Functor.map_comp, toHoCat_map_eq_iff] using h.postcomp _

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.RightHomotopyRel.postcomp, CategoryTheory.Functor.map_comp
-- 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
⊢ Functor.obj bifibrantResolution (Functor.obj toHoCat X) = Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj

Tactic:
rfl

Premises used: 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 : X ⟶ Y
⊢ Eq (α :=
    Functor.obj bifibrantResolution (Functor.obj toHoCat X) ⟶ Functor.obj bifibrantResolution (Functor.obj toHoCat Y))
    (CategoryTheory.Functor.map bifibrantResolution (CategoryTheory.Functor.map toHoCat f))
    (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap f))

Tactic:
rfl

Premises used: 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
⊢ NatTrans.app adjUnit (Functor.obj toHoCat X) = CategoryTheory.Functor.map toHoCat X.iBifibrantResolutionObj

Tactic:
rfl

Premises used: 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), WeakEquivalence (NatTrans.app HoCat.adjUnit (Functor.obj toHoCat X))
⊢ WeakEquivalence (NatTrans.app HoCat.adjUnit 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
rw : WeakEquivalence X.iBifibrantResolutionObj.hom
⊢ WeakEquivalence (NatTrans.app HoCat.adjUnit (Functor.obj toHoCat X))

Tactic:
rw [HoCat.adjUnit_app, weakEquivalence_toHoCat_map_iff,
    weakEquivalence_iff_of_objectProperty]

Premises used: HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, 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₁ X₂ : BifibrantObject.{v, u} C
f : X₁ ⟶ X₂
⊢ 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)))))

Tactic:
have := (ObjectProperty.ι _).congr_map
          (bifibrantResolutionMap_fac (CofibrantObject.homMk f.hom)).symm
-- 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 :
  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))))
⊢ Eq (α :=
    X₁ ⟶
      (Functor.obj BifibrantObject.HoCat.ιCofibrantObject
              (Functor.obj (Quotient.functor (BifibrantObject.homRel C)) X₂)).as
          (r := homRel C).bifibrantResolutionObj)
    (f ≫
      BifibrantObject.homMk (InducedCategory.Hom.hom (iBifibrantResolutionObj (mk (X₂.obj (P := bifibrantObjects C))))))
    (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:
ext : 1