awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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)))))
⊢ 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))))
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.HoCat.{v, u} C
⊢ IsIso (NatTrans.app HoCat.adjCounit' X)
have obtain : ∀ (X : BifibrantObject.{v, u} C), IsIso (NatTrans.app HoCat.adjCounit' (Functor.obj BifibrantObject.toHoCat X))
Tactic: obtain ⟨X, rfl⟩ := BifibrantObject.toHoCat_obj_surjective X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.{v, u} C
⊢ IsIso (NatTrans.app HoCat.adjCounit' (Functor.obj BifibrantObject.toHoCat X))
have 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)))))))))
Tactic: rw [HoCat.adjCounit'_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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))))))
have 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)))))
Tactic: simp only [BifibrantObject.weakEquivalence_homMk_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.{v, u} 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)))))))))
have 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))))))
Tactic: have : WeakEquivalence (C := BifibrantObject C)
      (BifibrantObject.homMk ((mk X.obj).iBifibrantResolutionObj).hom) := by
    simp only [BifibrantObject.weakEquivalence_homMk_iff]
    infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : HoCat.{v, u} C
⊢ CategoryTheory.Functor.map bifibrantResolution (NatTrans.app adjUnit X) ≫
      NatTrans.app (Iso.hom adjCounitIso) (Functor.obj bifibrantResolution X) =
    𝟙 (Functor.obj bifibrantResolution X)
have 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))
Tactic: obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
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))
have 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))))
Tactic: obtain ⟨X, _, rfl⟩ := CofibrantObject.mk_surjective X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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 := 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))))
have 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)))))
Tactic: rw [comp_hom_eq_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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 := 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)))))
have 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))))
Tactic: push inv
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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 := 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))))
have 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)))))
Tactic: apply bifibrantResolutionObj_hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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 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)))))
have 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)))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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 BifibrantObject.HoCat.ιCofibrantObject
        (NatTrans.app (Iso.inv adjCounitIso) (Functor.obj BifibrantObject.toHoCat (bifibrantResolutionObj (mk X)))))
have 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))))))))
Tactic: simp only [HoCat.adjCounitIso_inv_app,
      BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, ObjectProperty.homMk_hom]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.HoCat.{v, u} C
⊢ 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)
have 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))
Tactic: obtain ⟨X, rfl⟩ := BifibrantObject.toHoCat_obj_surjective X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
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))
have 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)))
Tactic: rw [comp_hom_eq_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : BifibrantObject.{v, u} C
⊢ 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)))
have 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))
Tactic: push inv
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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)
have obtain : ∀ (X : CofibrantObject.{v, u} C), WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) (Functor.obj toHoCat X))
Tactic: obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : CofibrantObject.{v, u} C
⊢ WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) (Functor.obj toHoCat X))
have dsimp : WeakEquivalence (NatTrans.app HoCat.adjUnit (Functor.obj toHoCat X))
Tactic: dsimp [HoCat.adj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution X) (CategoryTheory.Functor.map HoCat.bifibrantResolution f)
have 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)
Tactic: obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
Cleared hypotheses: X, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
    (CategoryTheory.Functor.map HoCat.bifibrantResolution f)
have 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)
Tactic: obtain ⟨Y, rfl⟩ := toHoCat_obj_surjective Y
Cleared hypotheses: Y, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
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
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
    (CategoryTheory.Functor.map HoCat.bifibrantResolution f)
have 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))
Tactic: obtain ⟨f, rfl⟩ := toHoCat.map_surjective f
Cleared hypotheses: f, hf