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 Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hf : weakEquivalences (BifibrantObject.{v, u} C) f), weakEquivalences (BifibrantObject.{v, u} C) f
⊢ weakEquivalences (BifibrantObject.{v, u} C) f

Tactic:
rwa [weakEquivalence_iff] at hf

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : 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
rwa rwa₁ rwa₂ rwa₃ : homRel C (X := mk X) (Y := mk Y) (homMk x) (homMk 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)

Tactic:
rwa [toHoCat_map_eq_iff]

Premises used: HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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 :
  Quiver.Hom (V := BifibrantObject.{v, u} C) (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))
    (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk Y)))
h : HomRel.CompClosure (homRel C) x x_1
⊢ Eq.{v + 1} (α := RightHomotopyClass X Y)
    ((fun
          (f :
            Quiver.Hom (V := BifibrantObject.{v, u} C) (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))
              (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk Y)))) ↦
        (RightHomotopyClass.mk f.hom : RightHomotopyClass X Y))
      x)
    ((fun
          (f :
            Quiver.Hom (V := BifibrantObject.{v, u} C) (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))
              (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk Y)))) ↦
        (RightHomotopyClass.mk f.hom : RightHomotopyClass X Y))
      x_1)

Tactic:
simpa [RightHomotopyClass.mk_eq_mk_iff] using h

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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 : RightHomotopyClass X Y
f : X ⟶ Y
⊢ Eq (α := RightHomotopyClass X Y)
    (Quot.lift (r := HomRel.CompClosure (homRel C))
      (fun
          (f :
            Quiver.Hom (V := BifibrantObject.{v, u} C) (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))
              (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk Y)))) ↦
        RightHomotopyClass.mk f.hom)
      ⋯
      (Quot.lift (r := RightHomotopyRel) (fun (f : X ⟶ Y) ↦ CategoryTheory.Functor.map toHoCat (homMk f)) ⋯
        (Quot.mk RightHomotopyRel f)))
    (Quot.mk RightHomotopyRel f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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 : Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y))
f :
  Quiver.Hom (V := BifibrantObject.{v, u} C) (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))
    (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk Y)))
⊢ Eq (α := Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))
    (Quot.lift (r := RightHomotopyRel) (fun (f : X ⟶ Y) ↦ CategoryTheory.Functor.map toHoCat (homMk f)) ⋯
      (Quot.lift (r := HomRel.CompClosure (homRel C))
        (fun
            (f :
              Quiver.Hom (V := BifibrantObject.{v, u} C) (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk X)))
                (Quotient.as (r := homRel C) (Functor.obj toHoCat (mk Y)))) ↦
          RightHomotopyClass.mk f.hom)
        ⋯ (Quot.mk (HomRel.CompClosure (homRel C)) f)))
    (Quot.mk (HomRel.CompClosure (homRel C)) f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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
f : X ⟶ Y
⊢ Eq (α := Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))
    ((homEquivRight : (a : RightHomotopyClass X Y) → toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y))
        (RightHomotopyClass.mk f) :
      Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))
    (CategoryTheory.Functor.map toHoCat (homMk f) :
      Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))

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 : 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
f : X ⟶ Y
⊢ Eq (α := RightHomotopyClass X Y)
    ((Equiv.symm homEquivRight : (a : toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y)) → RightHomotopyClass X Y)
        (CategoryTheory.Functor.map toHoCat (homMk f)) :
      RightHomotopyClass X Y)
    (RightHomotopyClass.mk f : RightHomotopyClass X Y)

Tactic:
rfl

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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
f : X ⟶ Y
⊢ Eq (α := Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))
    ((homEquivLeft : (a : LeftHomotopyClass X Y) → toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y)) (LeftHomotopyClass.mk f) :
      Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))
    (CategoryTheory.Functor.map toHoCat (homMk f) :
      Quiver.Hom (V := HoCat.{v, u} C) (Functor.obj toHoCat (mk X)) (Functor.obj toHoCat (mk Y)))

Tactic:
simp [homEquivLeft]

Premises used: HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
x x_1 : BifibrantObject.{v, u} C
x_2 x_3 : x ⟶ x_1
h : homRel C x_2 x_3
⊢ Eq (α :=
    Functor.obj (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat) x ⟶
      Functor.obj (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat) x_1)
    (CategoryTheory.Functor.map (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat) x_2)
    (CategoryTheory.Functor.map (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat) x_3)

Tactic:
simpa [FibrantObject.toHoCat_map_eq_iff, FibrantObject.homRel_iff_leftHomotopyRel,
        homRel_iff_leftHomotopyRel] using h

Premises used: HomotopicalAlgebra.FibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRel, HomotopicalAlgebra.BifibrantObject.homRel_iff_leftHomotopyRel
-- 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
⊢ Functor.obj ιFibrantObject (Functor.obj toHoCat X) =
    Functor.obj FibrantObject.toHoCat (Functor.obj BifibrantObject.ιFibrantObject X)

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 : BifibrantObject.{v, u} C
f : X ⟶ Y
⊢ Eq (α := Functor.obj ιFibrantObject (Functor.obj toHoCat X) ⟶ Functor.obj ιFibrantObject (Functor.obj toHoCat Y))
    (CategoryTheory.Functor.map ιFibrantObject (CategoryTheory.Functor.map toHoCat f))
    (CategoryTheory.Functor.map FibrantObject.toHoCat (FibrantObject.homMk f.hom))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
x x_1 : BifibrantObject.{v, u} C
x_2 x_3 : x ⟶ x_1
h : homRel C x_2 x_3
⊢ Eq (α :=
    Functor.obj (BifibrantObject.ιCofibrantObject ⋙ CofibrantObject.toHoCat) x ⟶
      Functor.obj (BifibrantObject.ιCofibrantObject ⋙ CofibrantObject.toHoCat) x_1)
    (CategoryTheory.Functor.map (BifibrantObject.ιCofibrantObject ⋙ CofibrantObject.toHoCat) x_2)
    (CategoryTheory.Functor.map (BifibrantObject.ιCofibrantObject ⋙ CofibrantObject.toHoCat) x_3)

Tactic:
simpa [CofibrantObject.toHoCat_map_eq_iff]

Premises used: HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_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
⊢ Functor.obj ιCofibrantObject (Functor.obj toHoCat X) =
    Functor.obj CofibrantObject.toHoCat (Functor.obj BifibrantObject.ιCofibrantObject X)

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 : BifibrantObject.{v, u} C
f : X ⟶ Y
⊢ Eq (α := Functor.obj ιCofibrantObject (Functor.obj toHoCat X) ⟶ Functor.obj ιCofibrantObject (Functor.obj toHoCat Y))
    (CategoryTheory.Functor.map ιCofibrantObject (CategoryTheory.Functor.map toHoCat f))
    (CategoryTheory.Functor.map CofibrantObject.toHoCat (CofibrantObject.homMk f.hom))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, 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
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)))
⊢ IsCofibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
have := isCofibrant_of_cofibration h.i
-- 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
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))
rw : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ IsFibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
rw [isFibrant_iff_of_isTerminal h.p terminalIsTerminal]

Premises used: HomotopicalAlgebra.isFibrant_iff_of_isTerminal, CategoryTheory.MorphismProperty.MapFactorizationData.p, CategoryTheory.Limits.terminalIsTerminal
-- 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
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))
⊢ Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations 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 : 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))

Tactic:
have : IsFibrant h.Z := by
    rw [isFibrant_iff_of_isTerminal h.p terminalIsTerminal]
    infer_instance
-- 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
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_1 : IsCofibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : IsFibrant.{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)

Tactic:
⟨BifibrantObject.mk h.Z, homMk h.i, inferInstanceAs (Cofibration h.i),
    inferInstanceAs (WeakEquivalence h.i)⟩

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.Z, _private.0.HomotopicalAlgebra.CofibrantObject.exists_bifibrant._proof_2, HomotopicalAlgebra.CofibrantObject.homMk, And.intro, Exists.intro, HomotopicalAlgebra.BifibrantObject.mk, CategoryTheory.MorphismProperty.MapFactorizationData.i, _private.0.HomotopicalAlgebra.CofibrantObject.exists_bifibrant._proof_1
-- 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
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_1 : IsCofibrant.{v, u} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : IsFibrant.{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)

Tactic:
exact ⟨BifibrantObject.mk h.Z, homMk h.i, inferInstanceAs (Cofibration h.i),
    inferInstanceAs (WeakEquivalence h.i)⟩
-- 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
⊢ Cofibration X.iBifibrantResolutionObj.hom

Tactic:
(exists_bifibrant X).choose_spec.choose_spec.1

Premises used: Exists.choose_spec, And.left, HomotopicalAlgebra.cofibrantObjects, HomotopicalAlgebra.bifibrantObjects, HomotopicalAlgebra.CofibrantObject.exists_bifibrant
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : CofibrantObject.{v, u} C
⊢ WeakEquivalence X.iBifibrantResolutionObj.hom

Tactic:
(exists_bifibrant X).choose_spec.choose_spec.2

Premises used: Exists.choose_spec, And.right, HomotopicalAlgebra.cofibrantObjects, HomotopicalAlgebra.bifibrantObjects, HomotopicalAlgebra.CofibrantObject.exists_bifibrant
-- 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 X.iBifibrantResolutionObj

Tactic:
rw [weakEquivalence_iff_of_objectProperty]

Premises used: HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : CofibrantObject.{v, u} C
⊢ WeakEquivalence X.iBifibrantResolutionObj.hom

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
⊢ IsFibrant.{v, u} (Functor.obj ι (Functor.obj BifibrantObject.ιCofibrantObject X))

Tactic:
X.2.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.right, HomotopicalAlgebra.cofibrantObjects, HomotopicalAlgebra.bifibrantObjects, HomotopicalAlgebra.fibrantObjects
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
⊢ Eq (α := Functor.obj ι X₁ ⟶ terminal.{v, u} C)
    (CategoryTheory.Functor.map ι (f ≫ X₂.iBifibrantResolutionObj) ≫
      terminal.from (Functor.obj ι (Functor.obj BifibrantObject.ιCofibrantObject X₂.bifibrantResolutionObj)))
    (X₁.iBifibrantResolutionObj.hom ≫
      terminal.from
        ((Functor.obj BifibrantObject.ιCofibrantObject X₁.bifibrantResolutionObj).obj (P := cofibrantObjects C)))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
⊢ 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⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
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)))
⊢ ∃ (g : X₁.bifibrantResolutionObj ⟶ X₂.bifibrantResolutionObj),
    X₁.iBifibrantResolutionObj ≫ CategoryTheory.Functor.map BifibrantObject.ιCofibrantObject g =
      f ≫ X₂.iBifibrantResolutionObj

Tactic:
exact ⟨BifibrantObject.homMk sq.lift, by cat_disch⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
⊢ X₁.iBifibrantResolutionObj ≫ homMk (bifibrantResolutionMap f).hom = f ≫ X₂.iBifibrantResolutionObj

Tactic:
(exists_bifibrant_map f).choose_spec

Premises used: Exists.choose_spec, HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map, CategoryTheory.ObjectProperty.homMk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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
rw : weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)
⊢ WeakEquivalence (bifibrantResolutionMap f)

Tactic:
rw [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X₁ X₂ : CofibrantObject.{v, u} C
f : X₁ ⟶ X₂
inst_2 : WeakEquivalence f
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)
⊢ weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)

Tactic:
change weakEquivalences _ (CofibrantObject.homMk (bifibrantResolutionMap f).hom)

Premises used: HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap, HomotopicalAlgebra.CofibrantObject.homMk, CategoryTheory.InducedCategory.Hom.hom, HomotopicalAlgebra.weakEquivalences
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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
rw : WeakEquivalence X₂.iBifibrantResolutionObj
⊢ 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:
rw [← weakEquivalence_iff, ← weakEquivalence_precomp_iff (iBifibrantResolutionObj X₁),
    bifibrantResolutionMap_fac, weakEquivalence_precomp_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj, HomotopicalAlgebra.weakEquivalence_precomp_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
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 X₂.iBifibrantResolutionObj

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

Tactic:
toHoCat.congr_map (bifibrantResolutionMap_fac f)

Premises used: HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, HomotopicalAlgebra.CofibrantObject.toHoCat, CategoryTheory.Quotient.comp, CategoryTheory.Functor.congr_map