awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
inst_2 : IsFibrant.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
⊢ _root_.Equivalence fun (x1 x2 : X ⟶ Y) ↦ homRel C x1 x2

Tactic:
(RightHomotopyRel.equivalence _ _).comap (fun (f : X ⟶ Y) ↦ f.hom)

Premises used: HomotopicalAlgebra.CofibrantObject.homRel, HomotopicalAlgebra.RightHomotopyRel.equivalence, CategoryTheory.InducedCategory.Hom.hom, Equivalence.comap
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := CofibrantObject.{v_1, u_1} C) (Functor.obj toHoCat)

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

Premises used: Exists, _private.0.HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective.match_1, HomotopicalAlgebra.CofibrantObject.toHoCat, Exists.intro, Eq, Function.Surjective, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ Functor.Full.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) (D := HoCat.{v_1, u_1} C)
    (Quotient.functor (homRel C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} 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.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
inst_2 : IsFibrant.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
f g : X ⟶ Y
rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
rw₁ : Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
rw₂ : Relation.EqvGen (homRel C) f g ↔ homRel C f g
rw₃ rw₄ : (fun (x1 x2 : X ⟶ Y) ↦ homRel C x1 x2) f g ↔ homRel C f g
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g

Tactic:
rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isFibrant_tgt.eqvGen_eq]

Premises used: HomotopicalAlgebra.CofibrantObject.homRel_equivalence_of_isFibrant_tgt, CategoryTheory.Functor.homRel_iff, CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen, CategoryTheory.HomRel.compClosure_eq_self, Equivalence.eqvGen_eq
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
simp : WeakEquivalence f.hom ↔ WeakEquivalence g.hom
⊢ weakEquivalences (CofibrantObject.{v_1, u_1} C) f ↔ weakEquivalences (CofibrantObject.{v_1, u_1} C) g

Tactic:
simp only [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]

Premises used: HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
obtain :
  ∀ (P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))) (h : P.RightHomotopy f.hom g.hom),
    WeakEquivalence f.hom ↔ WeakEquivalence g.hom
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
h : P.RightHomotopy f.hom g.hom
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom

Tactic:
apply h.weakEquivalence_iff

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f : X ⟶ Y
simp :
  weakEquivalences (HoCat.{v_1, u_1} C) (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f) ↔
    weakEquivalences (CofibrantObject.{v_1, u_1} C) f
⊢ WeakEquivalence (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f : X ⟶ Y
⊢ weakEquivalences (HoCat.{v_1, u_1} C) (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f) ↔
    weakEquivalences (CofibrantObject.{v_1, u_1} C) f

Tactic:
apply MorphismProperty.quotient_iff

Premises used: CategoryTheory.MorphismProperty.quotient_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : CofibrantObject.{v_1, u_1} C
x_2 : x ⟶ x_1
h : weakEquivalences (CofibrantObject.{v_1, u_1} C) x_2
⊢ WeakEquivalence x_2

Tactic:
simp only [← weakEquivalence_iff] at h

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : CofibrantObject.{v_1, u_1} C
x_2 : x ⟶ x_1
h : WeakEquivalence x_2
⊢ MorphismProperty.inverseImage (weakEquivalences (HoCat.{v_1, u_1} C)) toHoCat x_2

Tactic:
simpa only [MorphismProperty.inverseImage_iff, ← weakEquivalence_iff,
      weakEquivalence_toHoCat_map_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff, CategoryTheory.MorphismProperty.inverseImage_iff, HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
obtain :
  ∀ (P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))),
    P.IsVeryGood →
      ∀ (h : P.RightHomotopy f.hom g.hom),
        AreEqualizedByLocalization (weakEquivalences (CofibrantObject.{v_1, u_1} C)) f g
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject.{v_1, u_1} C)) f g

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

Premises used: HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
rw : L.map f = L.map g
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject.{v_1, u_1} C)) f g

Tactic:
rw [areEqualizedByLocalization_iff L]

Premises used: CategoryTheory.areEqualizedByLocalization_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
this : Eq (α := L.obj (mk P.P) ⟶ L.obj (mk (Y.obj (P := cofibrantObjects C)))) (L.map (homMk P.p₀)) (L.map (homMk P.p₁))
⊢ L.map f = L.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, this]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
suffices :
  Eq (α := L.obj (mk P.P) ⟶ L.obj (mk (Y.obj (P := cofibrantObjects C)))) (L.map (homMk P.p₀)) (L.map (homMk P.p₁))
⊢ L.map f = L.map g

Tactic:
suffices L.map (homMk P.p₀) = L.map (homMk P.p₁) by
    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, this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
simp : WeakEquivalence P.ι
⊢ weakEquivalences (CofibrantObject.{v_1, u_1} C) (X := mk (Y.obj (P := cofibrantObjects C))) (Y := mk P.P) (homMk P.ι)

Tactic:
simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.CofibrantObject.weakEquivalence_homMk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
⊢ WeakEquivalence P.ι

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
⊢ IsIso (X := L.obj (mk (Y.obj (P := cofibrantObjects C)))) (Y := L.obj (mk P.P)) (L.map (homMk P.ι))

Tactic:
have := Localization.inverts L (weakEquivalences _) (homMk P.ι) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
this : IsIso (X := L.obj (mk (Y.obj (P := cofibrantObjects C)))) (Y := L.obj (mk P.P)) (L.map (homMk P.ι))
⊢ Eq (α := L.obj (mk P.P) ⟶ L.obj (mk (Y.obj (P := cofibrantObjects C)))) (L.map (homMk P.p₀)) (L.map (homMk P.p₁))

Tactic:
simp only [← cancel_epi (L.map (homMk P.ι)), ← L.map_comp, homMk_homMk, P.ι_p₀, P.ι_p₁]

Premises used: HomotopicalAlgebra.CofibrantObject.homMk_homMk, HomotopicalAlgebra.PathObject.toPrepathObject, CategoryTheory.Functor.map, HomotopicalAlgebra.CofibrantObject.homMk, CategoryTheory.Functor.map_comp, HomotopicalAlgebra.PrepathObject.ι_p₀, CategoryTheory.cancel_epi, HomotopicalAlgebra.PrepathObject.ι_p₁, HomotopicalAlgebra.PrepathObject.ι
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
apply :
  Eq (α := MorphismProperty.{v_1, u_1} (CofibrantObject.{v_1, u_1} C)) (weakEquivalences (CofibrantObject.{v_1, u_1} C))
    (MorphismProperty.inverseImage (D :=
      CategoryTheory.Quotient.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C) (homRel C))
      (weakEquivalences (HoCat.{v_1, u_1} C)) (Quotient.functor (homRel C)))
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences (HoCat.{v_1, u_1} C)) (toHoCatLocalizerMorphism C)

Tactic:
apply (factorsThroughLocalization C).isLocalizedEquivalence

Premises used: HomRel.FactorsThroughLocalization.isLocalizedEquivalence, HomotopicalAlgebra.CofibrantObject.factorsThroughLocalization
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ Eq (α := MorphismProperty.{v_1, u_1} (CofibrantObject.{v_1, u_1} C)) (weakEquivalences (CofibrantObject.{v_1, u_1} C))
    (MorphismProperty.inverseImage (D :=
      CategoryTheory.Quotient.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C) (homRel C))
      (weakEquivalences (HoCat.{v_1, u_1} C)) (Quotient.functor (homRel C)))

Tactic:
apply MorphismProperty.eq_inverseImage_quotientFunctor

Premises used: CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
⊢ (toHoCat ⋙ L).IsLocalization (weakEquivalences (CofibrantObject.{v_1, u_1} C))

Tactic:
inferInstanceAs (((toHoCatLocalizerMorphism C).functor ⋙ L).IsLocalization _)

Premises used: _private.0.HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
have :
  ∀
    (h :
      MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X :=
        initial.{v_1, u_1} C) (initial.to X)),
    ∃ (X' : C) (_ : IsCofibrant.{v_1, u_1} X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p
⊢ ∃ (X' : C) (_ : IsCofibrant.{v_1, u_1} X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p

Tactic:
have h := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C)
    (initial.to X)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
h :
  MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X := initial.{v_1, u_1} C)
    (initial.to X)
⊢ ∃ (X' : C) (_ : IsCofibrant.{v_1, u_1} X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p

Tactic:
⟨h.Z, ?_, h.p, inferInstance, inferInstance⟩

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.Z, CategoryTheory.MorphismProperty.MapFactorizationData.p, inferInstance, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
h :
  MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X := initial.{v_1, u_1} C)
    (initial.to X)
refine : IsCofibrant.{v_1, u_1} (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ ∃ (X' : C) (_ : IsCofibrant.{v_1, u_1} X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p

Tactic:
refine ⟨h.Z, ?_, h.p, inferInstance, inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
h :
  MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X := initial.{v_1, u_1} C)
    (initial.to X)
rw : Cofibration (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ IsCofibrant.{v_1, u_1} (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
rw [isCofibrant_iff_of_isInitial h.i initialIsInitial]

Premises used: CategoryTheory.Limits.initialIsInitial, HomotopicalAlgebra.isCofibrant_iff_of_isInitial, CategoryTheory.MorphismProperty.MapFactorizationData.i
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
h :
  MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X := initial.{v_1, u_1} C)
    (initial.to X)
⊢ Cofibration (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ IsCofibrant.{v_1, u_1} (HoCat.resolutionObj.{v_1, u_1} X)

Tactic:
(HoCat.exists_resolution X).choose_spec.choose

Premises used: Exists.choose_spec, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj, Exists.choose, HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ Fibration.{v_1, u_1} (X := HoCat.resolutionObj.{v_1, u_1} X) (HoCat.pResolutionObj X)

Tactic:
(HoCat.exists_resolution X).choose_spec.choose_spec.choose_spec.1

Premises used: Exists.choose_spec, HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj, And.left, HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ WeakEquivalence.{v_1, u_1} (X := HoCat.resolutionObj.{v_1, u_1} X) (HoCat.pResolutionObj X)

Tactic:
(HoCat.exists_resolution X).choose_spec.choose_spec.choose_spec.2

Premises used: Exists.choose_spec, HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj, And.right, HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
inst_2 : IsFibrant.{v_1, u_1} X
⊢ IsFibrant.{v_1, u_1} (HoCat.resolutionObj.{v_1, u_1} X)

Tactic:
isFibrant_of_fibration (HoCat.pResolutionObj X)

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj, HomotopicalAlgebra.isFibrant_of_fibration
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := initial.{v_1, u_1} C ⟶ Y) (initial.to (resolutionObj.{v_1, u_1} Y) ≫ pResolutionObj Y)
    (initial.to (resolutionObj.{v_1, u_1} X) ≫ pResolutionObj X ≫ f)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ CommSq (W := initial.{v_1, u_1} C) (initial.to (resolutionObj.{v_1, u_1} Y)) (initial.to (resolutionObj.{v_1, u_1} X))
    (pResolutionObj Y) (pResolutionObj X ≫ f)

Tactic:
have sq : CommSq (initial.to _) (initial.to _) (pResolutionObj Y)
    (pResolutionObj X ≫ f) := ⟨by simp⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
sq :
  CommSq (W := initial.{v_1, u_1} C) (initial.to (resolutionObj.{v_1, u_1} Y)) (initial.to (resolutionObj.{v_1, u_1} X))
    (pResolutionObj Y) (pResolutionObj X ≫ f)
⊢ ∃ (g : resolutionObj.{v_1, u_1} X ⟶ resolutionObj.{v_1, u_1} Y), g ≫ pResolutionObj Y = pResolutionObj X ≫ f

Tactic:
⟨sq.lift, sq.fac_right⟩

Premises used: CategoryTheory.CommSq.lift, CategoryTheory.CommSq.fac_right, Exists.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
sq :
  CommSq (W := initial.{v_1, u_1} C) (initial.to (resolutionObj.{v_1, u_1} Y)) (initial.to (resolutionObj.{v_1, u_1} X))
    (pResolutionObj Y) (pResolutionObj X ≫ f)
⊢ ∃ (g : resolutionObj.{v_1, u_1} X ⟶ resolutionObj.{v_1, u_1} Y), g ≫ pResolutionObj Y = pResolutionObj X ≫ f

Tactic:
exact ⟨sq.lift, sq.fac_right⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := resolutionObj.{v_1, u_1} X ⟶ Y) (resolutionMap f ≫ pResolutionObj Y) (pResolutionObj X ≫ f)

Tactic:
(exists_resolution_map f).choose_spec

Premises used: Exists.choose_spec, HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution_map, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
rw : WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f ≫ pResolutionObj Y) ↔ WeakEquivalence f
rw₁ : WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (pResolutionObj X ≫ f) ↔ WeakEquivalence f
rw₂ rw₃ : WeakEquivalence f ↔ WeakEquivalence f
⊢ WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f) ↔ WeakEquivalence f

Tactic:
rw [← weakEquivalence_postcomp_iff _ (pResolutionObj Y),
    HoCat.resolutionMap_fac, weakEquivalence_precomp_iff]

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac, HomotopicalAlgebra.weakEquivalence_precomp_iff, HomotopicalAlgebra.weakEquivalence_postcomp_iff