awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
simp : WeakEquivalence f.hom ↔ WeakEquivalence g.hom
⊢ weakEquivalences (FibrantObject.{v_1, u_1} C) f ↔ weakEquivalences (FibrantObject.{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.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
obtain :
  ∀ (P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))) (h : P.LeftHomotopy 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.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
h : P.LeftHomotopy f.hom g.hom
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom

Tactic:
apply h.weakEquivalence_iff

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{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 (FibrantObject.{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.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{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 (FibrantObject.{v_1, u_1} C) f

Tactic:
apply MorphismProperty.quotient_iff

Premises used: CategoryTheory.MorphismProperty.quotient_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : FibrantObject.{v_1, u_1} C
x_2 : x ⟶ x_1
h : weakEquivalences (FibrantObject.{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.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : FibrantObject.{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.FibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.weakEquivalence_iff, CategoryTheory.MorphismProperty.inverseImage_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
obtain :
  ∀ (P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))),
    P.IsVeryGood →
      ∀ (h : P.LeftHomotopy f.hom g.hom), AreEqualizedByLocalization (weakEquivalences (FibrantObject.{v_1, u_1} C)) f g
⊢ AreEqualizedByLocalization (weakEquivalences (FibrantObject.{v_1, u_1} C)) f g

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

Premises used: HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
rw : L.map f = L.map g
⊢ AreEqualizedByLocalization (weakEquivalences (FibrantObject.{v_1, u_1} C)) f g

Tactic:
rw [areEqualizedByLocalization_iff L]

Premises used: CategoryTheory.areEqualizedByLocalization_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
this : Eq (α := L.obj (mk (X.obj (P := fibrantObjects C))) ⟶ L.obj (mk P.I)) (L.map (homMk P.i₀)) (L.map (homMk P.i₁))
⊢ L.map f = L.map g

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

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

Tactic:
suffices L.map (homMk P.i₀) = L.map (homMk P.i₁) by
    simp only [show f = homMk P.i₀ ≫ homMk h.h by cat_disch,
      show g = homMk P.i₁ ≫ homMk h.h by cat_disch, Functor.map_comp, this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
simp : WeakEquivalence P.π
⊢ weakEquivalences (FibrantObject.{v_1, u_1} C) (X := mk P.I) (Y := mk (X.obj (P := fibrantObjects C))) (homMk P.π)

Tactic:
simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.FibrantObject.weakEquivalence_homMk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
⊢ WeakEquivalence P.π

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
⊢ IsIso (X := L.obj (mk P.I)) (Y := L.obj (mk (X.obj (P := fibrantObjects C)))) (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.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
this : IsIso (X := L.obj (mk P.I)) (Y := L.obj (mk (X.obj (P := fibrantObjects C)))) (L.map (homMk P.π))
⊢ Eq (α := L.obj (mk (X.obj (P := fibrantObjects C))) ⟶ L.obj (mk P.I)) (L.map (homMk P.i₀)) (L.map (homMk P.i₁))

Tactic:
simp [← cancel_mono (L.map (homMk P.π)), ← L.map_comp]

Premises used: HomotopicalAlgebra.Precylinder.π, CategoryTheory.cancel_mono, HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, HomotopicalAlgebra.FibrantObject.homMk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (FibrantObject.{v_1, u_1} C)) (weakEquivalences (FibrantObject.{v_1, u_1} C))
    (MorphismProperty.inverseImage (D :=
      CategoryTheory.Quotient.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C) (homRel C))
      (weakEquivalences (HoCat.{v_1, u_1} C)) (Quotient.functor (homRel C)))
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{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.FibrantObject.factorsThroughLocalization
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (FibrantObject.{v_1, u_1} C)) (weakEquivalences (FibrantObject.{v_1, u_1} C))
    (MorphismProperty.inverseImage (D :=
      CategoryTheory.Quotient.{v_1, u_1} (C := FibrantObject.{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.FibrantObjectHomotopy
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 (FibrantObject.{v_1, u_1} C))

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

Premises used: _private.0.HomotopicalAlgebra.FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (trivialCofibrations C) (fibrations C) (Y :=
        terminal.{v_1, u_1} C) (terminal.from X)),
    ∃ (X' : C) (_ : IsFibrant.{v_1, u_1} X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i
⊢ ∃ (X' : C) (_ : IsFibrant.{v_1, u_1} X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i

Tactic:
have h := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C)
    (terminal.from X)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (trivialCofibrations C) (fibrations C) (Y := terminal.{v_1, u_1} C)
    (terminal.from X)
⊢ ∃ (X' : C) (_ : IsFibrant.{v_1, u_1} X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i

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

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.Z, inferInstance, And.intro, Exists.intro, CategoryTheory.MorphismProperty.MapFactorizationData.i
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (trivialCofibrations C) (fibrations C) (Y := terminal.{v_1, u_1} C)
    (terminal.from X)
refine : IsFibrant.{v_1, u_1} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ ∃ (X' : C) (_ : IsFibrant.{v_1, u_1} X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i

Tactic:
refine ⟨h.Z, ?_, h.i, inferInstance, inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (trivialCofibrations C) (fibrations C) (Y := terminal.{v_1, u_1} C)
    (terminal.from X)
rw : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ IsFibrant.{v_1, u_1} (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.FibrantObjectHomotopy
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} (trivialCofibrations C) (fibrations C) (Y := terminal.{v_1, u_1} C)
    (terminal.from X)
⊢ Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ IsFibrant.{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.FibrantObject.HoCat.exists_resolution, HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj, Exists.choose
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ Cofibration.{v_1, u_1} (Y := HoCat.resolutionObj.{v_1, u_1} X) (HoCat.iResolutionObj X)

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

Premises used: Exists.choose_spec, HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution, And.left, HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (Y := HoCat.resolutionObj.{v_1, u_1} X) (HoCat.iResolutionObj X)

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

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

Tactic:
isCofibrant_of_cofibration (HoCat.iResolutionObj X)

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, HomotopicalAlgebra.isCofibrant_of_cofibration
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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 (α := X ⟶ terminal.{v_1, u_1} C) ((f ≫ iResolutionObj Y) ≫ terminal.from (resolutionObj.{v_1, u_1} Y))
    (iResolutionObj X ≫ terminal.from (resolutionObj.{v_1, u_1} X))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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 (Z := terminal.{v_1, u_1} C) (f ≫ iResolutionObj Y) (iResolutionObj X)
    (terminal.from (resolutionObj.{v_1, u_1} Y)) (terminal.from (resolutionObj.{v_1, u_1} X))

Tactic:
have sq : CommSq (f ≫ iResolutionObj Y) (iResolutionObj X)
    (terminal.from _) (terminal.from _) := ⟨by simp⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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 (Z := terminal.{v_1, u_1} C) (f ≫ iResolutionObj Y) (iResolutionObj X)
    (terminal.from (resolutionObj.{v_1, u_1} Y)) (terminal.from (resolutionObj.{v_1, u_1} X))
⊢ ∃ (g : resolutionObj.{v_1, u_1} X ⟶ resolutionObj.{v_1, u_1} Y), iResolutionObj X ≫ g = f ≫ iResolutionObj Y

Tactic:
⟨sq.lift, sq.fac_left⟩

Premises used: CategoryTheory.CommSq.lift, Exists.intro, CategoryTheory.CommSq.fac_left
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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 (Z := terminal.{v_1, u_1} C) (f ≫ iResolutionObj Y) (iResolutionObj X)
    (terminal.from (resolutionObj.{v_1, u_1} Y)) (terminal.from (resolutionObj.{v_1, u_1} X))
⊢ ∃ (g : resolutionObj.{v_1, u_1} X ⟶ resolutionObj.{v_1, u_1} Y), iResolutionObj X ≫ g = f ≫ iResolutionObj Y

Tactic:
exact ⟨sq.lift, sq.fac_left⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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 (α := X ⟶ resolutionObj.{v_1, u_1} Y) (iResolutionObj X ≫ resolutionMap f) (f ≫ iResolutionObj Y)

Tactic:
(exists_resolution_map f).choose_spec

Premises used: Exists.choose_spec, HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution_map, HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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 (Y := resolutionObj.{v_1, u_1} Y) (iResolutionObj X ≫ resolutionMap f) ↔ WeakEquivalence f
rw₁ : WeakEquivalence (Y := resolutionObj.{v_1, u_1} Y) (f ≫ iResolutionObj Y) ↔ WeakEquivalence f
rw₂ rw₃ : WeakEquivalence f ↔ WeakEquivalence f
⊢ WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f) ↔ WeakEquivalence f

Tactic:
rw [← weakEquivalence_precomp_iff (iResolutionObj X),
    HoCat.resolutionMap_fac, weakEquivalence_postcomp_iff]

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac, HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, HomotopicalAlgebra.weakEquivalence_precomp_iff, HomotopicalAlgebra.weakEquivalence_postcomp_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
h₁ : homRel C (X := mk (resolutionObj.{v_1, u_1} X)) (Y := mk Y) (homMk f) (homMk g)
⊢ Eq (α :=
    Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} X)))
      (Functor.obj toHoCat (mk Y)))
    (CategoryTheory.Functor.map toHoCat (homMk f)) (CategoryTheory.Functor.map toHoCat (homMk g))

Tactic:
apply toHoCat_map_eq

Premises used: HomotopicalAlgebra.FibrantObject.toHoCat_map_eq
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
h₁ :
  RightHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
    (Y := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)) (InducedCategory.Hom.hom (homMk f))
    (InducedCategory.Hom.hom (homMk g))
⊢ LeftHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
    (Y := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)) (InducedCategory.Hom.hom (homMk f))
    (InducedCategory.Hom.hom (homMk g))

Tactic:
apply RightHomotopyRel.leftHomotopyRel

Premises used: HomotopicalAlgebra.RightHomotopyRel.leftHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
h₁ :
  ∀
    (h :
      Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk (iResolutionObj X ≫ f))
        (RightHomotopyClass.mk (iResolutionObj X ≫ g))),
    Eq (α :=
      RightHomotopyClass (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
        (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)))
      (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
      (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))
⊢ RightHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
    (Y := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)) (InducedCategory.Hom.hom (homMk f))
    (InducedCategory.Hom.hom (homMk g))

Tactic:
rw [← RightHomotopyClass.mk_eq_mk_iff] at h ⊢

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h :
  Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk (iResolutionObj X ≫ f))
    (RightHomotopyClass.mk (iResolutionObj X ≫ g))
⊢ Eq (α :=
    RightHomotopyClass (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
      (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)))
    (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
    (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))

Tactic:
(RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
    (f := iResolutionObj X) (Z := Y)).1 h

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence, And.left, Classical.choose, HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj