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 Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : RightHomotopyRel x x_1
⊢ Eq.{v + 1} (α := Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))
    ((fun (f : X ⟶ Y) ↦
        (CategoryTheory.Functor.map toHoCat (homMk f) :
          Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y))))
      x)
    ((fun (f : X ⟶ Y) ↦
        (CategoryTheory.Functor.map toHoCat (homMk f) :
          Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y))))
      x_1)
have rwa : homRel C (X := mk X) (Y := mk Y) (homMk x) (homMk x_1)
Tactic: rwa [toHoCat_map_eq_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 : CofibrantObject.{v, u} C
h : MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := terminal.{v, u} C)
  (terminal.from (X.obj (P := cofibrantObjects C))) :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C)
    (terminal.from (X.obj (P := cofibrantObjects C)))
⊢ ∃ (Y : BifibrantObject.{v, u} C) (i : X ⟶ Functor.obj BifibrantObject.ιCofibrantObject Y),
    Cofibration (X := Functor.obj ι X) (CategoryTheory.Functor.map ι i) ∧
      WeakEquivalence (X := Functor.obj ι X) (CategoryTheory.Functor.map ι i)
have this : IsCofibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: have := isCofibrant_of_cofibration h.i
-- 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
h : MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := terminal.{v, u} C)
  (terminal.from (X.obj (P := cofibrantObjects C))) :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C)
    (terminal.from (X.obj (P := cofibrantObjects C)))
this : IsCofibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ IsFibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
have rw : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: rw [isFibrant_iff_of_isTerminal h.p terminalIsTerminal]
-- 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 : CofibrantObject.{v, u} C
h : MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := terminal.{v, u} C)
  (terminal.from (X.obj (P := cofibrantObjects C))) :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C)
    (terminal.from (X.obj (P := cofibrantObjects C)))
this : IsCofibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ ∃ (Y : BifibrantObject.{v, u} C) (i : X ⟶ Functor.obj BifibrantObject.ιCofibrantObject Y),
    Cofibration (X := Functor.obj ι X) (CategoryTheory.Functor.map ι i) ∧
      WeakEquivalence (X := Functor.obj ι X) (CategoryTheory.Functor.map ι i)
have this₁ : IsFibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: have : IsFibrant h.Z := by
    rw [isFibrant_iff_of_isTerminal h.p terminalIsTerminal]
    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 : CofibrantObject.{v, u} C
⊢ WeakEquivalence X.iBifibrantResolutionObj
have rw : WeakEquivalence X.iBifibrantResolutionObj.hom
Tactic: rw [weakEquivalence_iff_of_objectProperty]
-- 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₁ X₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
⊢ ∃ (g : X₁.bifibrantResolutionObj ⟶ X₂.bifibrantResolutionObj),
    X₁.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g =
      f ≫ X₂.iBifibrantResolutionObj
have sq : CommSq (Z := terminal.{v, u} C) (CategoryTheory.Functor.map ι (f ≫ X₂.iBifibrantResolutionObj))
  X₁.iBifibrantResolutionObj.hom
  (terminal.from (Functor.obj ι (Functor.obj BifibrantObject.ιCofibrantObject X₂.bifibrantResolutionObj)))
  (terminal.from
    ((Functor.obj BifibrantObject.ιCofibrantObject X₁.bifibrantResolutionObj).obj (P := cofibrantObjects C)))
Tactic: have sq : CommSq (ι.map (f ≫ iBifibrantResolutionObj X₂))
    (iBifibrantResolutionObj X₁).hom (terminal.from _) (terminal.from _) := ⟨by simp⟩
-- 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₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
inst_2 : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)
have rw : weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)
Tactic: rw [weakEquivalence_iff]
-- 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₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
inst_2 : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)
have change : weakEquivalences (CofibrantObject.{v, u} C) (X := mk (X₁.bifibrantResolutionObj.obj (P := bifibrantObjects C))) (Y :=
  mk (X₂.bifibrantResolutionObj.obj (P := bifibrantObjects C))) (homMk (bifibrantResolutionMap f).hom)
Tactic: change weakEquivalences _ (CofibrantObject.homMk (bifibrantResolutionMap f).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₁ X₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
inst_2 : WeakEquivalence f
⊢ weakEquivalences (CofibrantObject.{v, u} C) (X := mk (X₁.bifibrantResolutionObj.obj (P := bifibrantObjects C))) (Y :=
    mk (X₂.bifibrantResolutionObj.obj (P := bifibrantObjects C))) (homMk (bifibrantResolutionMap f).hom)
have rw : WeakEquivalence X₂.iBifibrantResolutionObj
Tactic: rw [← weakEquivalence_iff, ← weakEquivalence_precomp_iff (iBifibrantResolutionObj X₁),
    bifibrantResolutionMap_fac, weakEquivalence_precomp_iff]
-- 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
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)
⊢ f = g
have 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
Tactic: obtain ⟨Y, rfl⟩ := BifibrantObject.toHoCat_obj_surjective Y
Cleared hypotheses: Y, f, g, h
-- 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
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
have 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
Tactic: obtain ⟨f, rfl⟩ := BifibrantObject.toHoCat.map_surjective f
Cleared hypotheses: f, h
-- 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
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)
⊢ CategoryTheory.Functor.map BifibrantObject.toHoCat f = g
have 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)
Tactic: obtain ⟨g, rfl⟩ := BifibrantObject.toHoCat.map_surjective g
Cleared hypotheses: g, h
-- 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 : 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 BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y)
    (CategoryTheory.Functor.map BifibrantObject.toHoCat f) (CategoryTheory.Functor.map BifibrantObject.toHoCat g)
have 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))
Tactic: change toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f) =
    toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g) at h
Cleared hypotheses: h
-- 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 : 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 (α := Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y)
    (CategoryTheory.Functor.map BifibrantObject.toHoCat f) (CategoryTheory.Functor.map BifibrantObject.toHoCat g)
have 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)
Tactic: rw [CofibrantObject.toHoCat_map_eq_iff,
    CofibrantObject.homRel_iff_rightHomotopyRel,
    ← RightHomotopyClass.mk_eq_mk_iff] at h
Cleared hypotheses: h
-- 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
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 (α := Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶ Functor.obj BifibrantObject.toHoCat Y)
    (CategoryTheory.Functor.map BifibrantObject.toHoCat f) (CategoryTheory.Functor.map BifibrantObject.toHoCat g)
have rw : Eq (α := RightHomotopyClass (X.bifibrantResolutionObj.obj (P := bifibrantObjects C)) (Y.obj (P := bifibrantObjects C)))
  (RightHomotopyClass.mk f.hom) (RightHomotopyClass.mk g.hom)
Tactic: rw [BifibrantObject.toHoCat_map_eq_iff,
    BifibrantObject.homRel_iff_rightHomotopyRel,
    ← RightHomotopyClass.mk_eq_mk_iff]
-- 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
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 (α :=
    RightHomotopyClass (X.bifibrantResolutionObj.obj (P := bifibrantObjects C)) (Y.obj (P := bifibrantObjects C)))
    (RightHomotopyClass.mk f.hom) (RightHomotopyClass.mk g.hom)
have 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))
Tactic: apply (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
    _ (iBifibrantResolutionObj X).hom).1
-- 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 g : X ⟶ Y
h : homRel C f g
⊢ Eq (α := Functor.obj bifibrantResolution' X ⟶ Functor.obj bifibrantResolution' Y)
    (CategoryTheory.Functor.map bifibrantResolution' f) (CategoryTheory.Functor.map bifibrantResolution' g)
have 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))
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 : HoCat.{v, u} C
⊢ WeakEquivalence (NatTrans.app HoCat.adjUnit X)
have obtain : ∀ (X : CofibrantObject.{v, u} C), WeakEquivalence (NatTrans.app HoCat.adjUnit (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 HoCat.adjUnit (Functor.obj toHoCat X))
have rw : WeakEquivalence X.iBifibrantResolutionObj.hom
Tactic: rw [HoCat.adjUnit_app, weakEquivalence_toHoCat_map_iff,
    weakEquivalence_iff_of_objectProperty]
-- 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₁ X₂ : BifibrantObject.{v, u} C
f : X₁ ⟶ X₂
⊢ 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)))
have 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)))))
Tactic: have := (ObjectProperty.ι _).congr_map
          (bifibrantResolutionMap_fac (CofibrantObject.homMk f.hom)).symm
-- 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 (α :=
    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)))
have 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))))
Tactic: ext : 1