awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
X : BifibrantObject.{v, u} C
⊢ IsFibrant.{v, u} ((Functor.obj ιCofibrantObject X).obj (P := cofibrantObjects C))

Tactic:
X.property.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 Y : BifibrantObject.{v, u} C
f g : X ⟶ Y
⊢ homRel C f g ↔ RightHomotopyRel f.hom g.hom

Tactic:
Iff.rfl

Premises used: Iff.rfl, HomotopicalAlgebra.BifibrantObject.homRel
-- 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 g : X ⟶ Y
rw : RightHomotopyRel f.hom g.hom ↔ LeftHomotopyRel f.hom g.hom
rw₁ rw₂ : RightHomotopyRel f.hom g.hom ↔ RightHomotopyRel f.hom g.hom
⊢ homRel C f g ↔ LeftHomotopyRel f.hom g.hom

Tactic:
rw [homRel_iff_rightHomotopyRel, leftHomotopyRel_iff_rightHomotopyRel]

Premises used: HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel, 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
⊢ Function.Surjective.{u + 1, u + 1} (α := BifibrantObject.{v, u} C) (Functor.obj toHoCat)

Tactic:
fun ⟨_⟩ ↦ ⟨_, rfl⟩

Premises used: Exists, HomotopicalAlgebra.BifibrantObject.toHoCat, Exists.intro, _private.0.HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective.match_1, Eq, Function.Surjective, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ Functor.Full.{v, v, u, u} (C := BifibrantObject.{v, u} C) (D := HoCat.{v, u} C) (Quotient.functor (homRel 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 Y : BifibrantObject.{v, u} C
f g : X ⟶ Y
h : homRel C f g
⊢ Eq (α := Functor.obj toHoCat X ⟶ Functor.obj toHoCat Y) (CategoryTheory.Functor.map toHoCat f)
    (CategoryTheory.Functor.map toHoCat g)

Tactic:
CategoryTheory.Quotient.sound _ h

Premises used: CategoryTheory.Quotient.sound
-- 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 g : X ⟶ Y
⊢ Eq (α := Functor.obj toHoCat X ⟶ Functor.obj toHoCat Y) (CategoryTheory.Functor.map toHoCat f)
      (CategoryTheory.Functor.map toHoCat g) ↔
    homRel C f g

Tactic:
Quotient.functor_map_eq_iff _ _ _

Premises used: CategoryTheory.Quotient.functor_map_eq_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} (CategoryTheory.Quotient.{v, u} (C := BifibrantObject.{v, u} C) (homRel C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
⊢ MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F ↔
    ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g

Tactic:
⟨fun H K L f g h ↦ ?_, fun h X Y f hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
refine_1 :
  ∀ (H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F) (K L : BifibrantObject.{v, u} C)
    (f g : K ⟶ L) (h : homRel C f g), F.map f = F.map g
refine_2 :
  ∀ (h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g)
    (X Y : BifibrantObject.{v, u} C) (f : X ⟶ Y) (hf : weakEquivalences (BifibrantObject.{v, u} C) f), IsIso (F.map f)
⊢ MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F ↔
    ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g

Tactic:
refine ⟨fun H K L f g h ↦ ?_, fun h X Y f hf ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h : homRel C f g
refine_1 :
  ∀ (P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))),
    P.IsVeryGood → ∀ (h : P.RightHomotopy f.hom g.hom), F.map f = F.map g
⊢ F.map f = F.map g

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject

Premises used: HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
⊢ IsCofibrant.{v, u} P.P

Tactic:
have := isCofibrant_of_cofibration P.ι
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant.{v, u} P.P
rw :
  WeakEquivalence (X :=
    ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk (L.obj (P := bifibrantObjects C)))) (Y :=
    ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk P.P)) (InducedCategory.Hom.hom (homMk P.ι))
⊢ weakEquivalences (BifibrantObject.{v, u} C) (X := mk (L.obj (P := bifibrantObjects C))) (Y := mk P.P) (homMk P.ι)

Tactic:
rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]

Premises used: HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant.{v, u} P.P
⊢ WeakEquivalence (X :=
    ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk (L.obj (P := bifibrantObjects C)))) (Y :=
    ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk P.P)) (InducedCategory.Hom.hom (homMk P.ι))

Tactic:
inferInstanceAs (WeakEquivalence P.ι)

Premises used: _private.0.HomotopicalAlgebra.BifibrantObject.inverts_iff_factors._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant.{v, u} P.P
⊢ WeakEquivalence (X :=
    ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk (L.obj (P := bifibrantObjects C)))) (Y :=
    ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk P.P)) (InducedCategory.Hom.hom (homMk P.ι))

Tactic:
exact inferInstanceAs (WeakEquivalence P.ι)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant.{v, u} P.P
⊢ IsIso (X := F.obj (mk (L.obj (P := bifibrantObjects C)))) (Y := F.obj (mk P.P)) (F.map (homMk P.ι))

Tactic:
have : IsIso (F.map (homMk P.ι)) := H _ (by
      rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
      exact inferInstanceAs (WeakEquivalence P.ι))
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this_1 : IsCofibrant.{v, u} P.P
this : IsIso (X := F.obj (mk (L.obj (P := bifibrantObjects C)))) (Y := F.obj (mk P.P)) (F.map (homMk P.ι))
refine_1 :
  Eq (α := F.obj K ⟶ F.obj L)
    (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₀)) : F.obj K ⟶ F.obj L)
    (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₁)) : F.obj K ⟶ F.obj L)
⊢ F.map f = F.map g

Tactic:
simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this_1 : IsCofibrant.{v, u} P.P
this : IsIso (X := F.obj (mk (L.obj (P := bifibrantObjects C)))) (Y := F.obj (mk P.P)) (F.map (homMk P.ι))
refine_1 :
  Eq (α := F.obj (mk P.P) ⟶ F.obj L) (F.map (homMk P.p₀) : F.obj (mk P.P) ⟶ F.obj L)
    (F.map (homMk P.p₁) : F.obj (mk P.P) ⟶ F.obj L)
⊢ Eq (α := F.obj K ⟶ F.obj L)
    (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₀)) : F.obj K ⟶ F.obj L)
    (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₁)) : F.obj K ⟶ F.obj L)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this_1 : IsCofibrant.{v, u} P.P
this : IsIso (X := F.obj (mk (L.obj (P := bifibrantObjects C)))) (Y := F.obj (mk P.P)) (F.map (homMk P.ι))
⊢ Eq (α := F.obj (mk P.P) ⟶ F.obj L) (F.map (homMk P.p₀) : F.obj (mk P.P) ⟶ F.obj L)
    (F.map (homMk P.p₁) : F.obj (mk P.P) ⟶ F.obj L)

Tactic:
simp [← cancel_epi (F.map (homMk P.ι)), ← Functor.map_comp]

Premises used: HomotopicalAlgebra.PathObject.toPrepathObject, CategoryTheory.Functor.map, HomotopicalAlgebra.BifibrantObject.homMk, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, HomotopicalAlgebra.PrepathObject.ι
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : weakEquivalences (BifibrantObject.{v, u} C) f
⊢ WeakEquivalence f.hom

Tactic:
rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty] at hf

Premises used: HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
refine_2 :
  ∀ (g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C))
    (h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C))))
    (h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))), IsIso (F.map f)
⊢ IsIso (F.map f)

Tactic:
obtain ⟨g', h₁, h₂⟩ := RightHomotopyClass.whitehead f.hom

Premises used: HomotopicalAlgebra.RightHomotopyClass.whitehead, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ IsIso (F.map f)

Tactic:
⟨F.map (homMk g'), ?_, ?_⟩

Premises used: CategoryTheory.Functor.map, HomotopicalAlgebra.BifibrantObject.homMk, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
refine_2 :
  Eq (α := F.obj X ⟶ F.obj X) (F.map f ≫ F.map (homMk g') : F.obj X ⟶ F.obj X) (𝟙 (F.obj X) : F.obj X ⟶ F.obj X)
refine_2₁ :
  Eq (α := F.obj Y ⟶ F.obj Y) (F.map (homMk g') ≫ F.map f : F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y) : F.obj Y ⟶ F.obj Y)
⊢ IsIso (F.map f)

Tactic:
refine ⟨F.map (homMk g'), ?_, ?_⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
refine_2 : F.map (f ≫ homMk g') = F.map (𝟙 X)
⊢ Eq (α := F.obj X ⟶ F.obj X) (F.map f ≫ F.map (homMk g') : F.obj X ⟶ F.obj X) (𝟙 (F.obj X) : F.obj X ⟶ F.obj X)

Tactic:
rw [← F.map_comp, ← F.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
refine_2 : homRel C (Y := X) (f ≫ homMk g' : X ⟶ X) (𝟙 X : X ⟶ X)
⊢ F.map (f ≫ homMk g') = F.map (𝟙 X)

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ homRel C (Y := X) (f ≫ homMk g' : X ⟶ X) (𝟙 X : X ⟶ X)

Tactic:
assumption
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
refine_2 : F.map (homMk g' ≫ f) = F.map (𝟙 Y)
⊢ Eq (α := F.obj Y ⟶ F.obj Y) (F.map (homMk g') ≫ F.map f : F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y) : F.obj Y ⟶ F.obj Y)

Tactic:
rw [← F.map_comp, ← F.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
refine_2 : homRel C (X := Y) (homMk g' ≫ f : Y ⟶ Y) (𝟙 Y : Y ⟶ Y)
⊢ F.map (homMk g' ≫ f) = F.map (𝟙 Y)

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ homRel C (X := Y) (homMk g' ≫ f : Y ⟶ Y) (𝟙 Y : Y ⟶ Y)

Tactic:
assumption
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
rw :
  ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L),
    homRel C f g →
      Eq (α := Functor.obj toHoCat K ⟶ Functor.obj toHoCat L) (CategoryTheory.Functor.map toHoCat f)
        (CategoryTheory.Functor.map toHoCat g)
⊢ MorphismProperty.IsInvertedBy.{v, v, u, u} (C := BifibrantObject.{v, u} C)
    (weakEquivalences (BifibrantObject.{v, u} C)) toHoCat

Tactic:
rw [inverts_iff_factors]

Premises used: HomotopicalAlgebra.BifibrantObject.inverts_iff_factors
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h : homRel C f g
⊢ Eq (α := Functor.obj toHoCat K ⟶ Functor.obj toHoCat L) (CategoryTheory.Functor.map toHoCat f)
    (CategoryTheory.Functor.map toHoCat g)

Tactic:
CategoryTheory.Quotient.sound _ h

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h : homRel C f g
⊢ Eq (α := Functor.obj toHoCat K ⟶ Functor.obj toHoCat L) (CategoryTheory.Functor.map toHoCat f)
    (CategoryTheory.Functor.map toHoCat g)

Tactic:
exact CategoryTheory.Quotient.sound _ h

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
hF : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hF : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g)
    (x y : BifibrantObject.{v, u} C) (f₁ f₂ : x ⟶ y), homRel C f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ (x y : BifibrantObject.{v, u} C) (f₁ f₂ : x ⟶ y), homRel C f₁ f₂ → F.map f₁ = F.map f₂

Tactic:
rwa [inverts_iff_factors] at hF

Premises used: HomotopicalAlgebra.BifibrantObject.inverts_iff_factors
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
⊢ Functor.IsLocalization.{v, u, v, u} (C := BifibrantObject.{v, u} C) toHoCat
    (weakEquivalences (BifibrantObject.{v, u} C))

Tactic:
.mk' _ _ strictUniversalPropertyFixedTargetToHoCat
    strictUniversalPropertyFixedTargetToHoCat

Premises used: HomotopicalAlgebra.BifibrantObject.strictUniversalPropertyFixedTargetToHoCat, CategoryTheory.Functor.IsLocalization.mk'