awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this : WeakEquivalence φ
have : ∀ (hp : RetractArrow (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)) φ), weakEquivalences C f
⊢ weakEquivalences C f

Tactic:
have hp : RetractArrow hf.p φ :=
      { i := Arrow.homMk (pushout.inl _ _) h.i.right
        r := Arrow.homMk (pushout.desc (𝟙 _) (h.r.left ≫ hf.i) (by simp)) h.r.right }
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this : WeakEquivalence φ
hp : RetractArrow (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)) φ
⊢ WeakEquivalence (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
have := mk'.cm3a_aux hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this_5 : WeakEquivalence φ
hp : RetractArrow (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)) φ
this : WeakEquivalence (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
rw :
  WeakEquivalence
    (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ weakEquivalences C f

Tactic:
rw [← weakEquivalence_iff, ← hf.fac]

Premises used: HomotopicalAlgebra.weakEquivalence_iff, CategoryTheory.MorphismProperty.MapFactorizationData.fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this_5 : WeakEquivalence φ
hp : RetractArrow (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)) φ
this : WeakEquivalence (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ WeakEquivalence
    (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
rw : IsStableUnderRetracts.{v, u} (rlp (trivialCofibrations C))
⊢ IsStableUnderRetracts.{v, u} (fibrations C)

Tactic:
rw [← rlp_eq_of_wfs (trivialCofibrations C) (fibrations C)]

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.rlp_eq_of_wfs, HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderRetracts.{v, u} (rlp (trivialCofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
rw : IsStableUnderRetracts.{v, u} (llp (trivialFibrations C))
⊢ IsStableUnderRetracts.{v, u} (cofibrations C)

Tactic:
rw [← llp_eq_of_wfs (cofibrations C) (trivialFibrations C)]

Premises used: HomotopicalAlgebra.cofibrations, CategoryTheory.MorphismProperty.llp_eq_of_wfs, HomotopicalAlgebra.trivialFibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderRetracts.{v, u} (llp (trivialFibrations C))

Tactic:
infer_instance
-- 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
X : C
inst_3 : IsCofibrant.{v, u} X
⊢ cofibrantObjects.{v, u} C X

Tactic:
assumption
-- 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
X : CofibrantObject.{v, u} C
⊢ ∃ (Y : C) (x : IsCofibrant.{v, u} Y), X = mk Y

Tactic:
⟨X.obj, X.property, rfl⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, Exists.intro, rfl
-- 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
X Y : C
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
f : Quiver.Hom (V := CofibrantObject.{v, u} C) (mk X) (mk Y)
⊢ ∃ (g : X ⟶ Y), f = homMk g

Tactic:
⟨f.hom, rfl⟩

Premises used: Exists.intro, CategoryTheory.InducedCategory.Hom.hom, rfl
-- 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 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_4 : IsCofibrant.{v, u} X
inst_5 : IsCofibrant.{v, u} Y
f : X ⟶ Y
simp : weakEquivalences (CofibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f
⊢ WeakEquivalence (C := CofibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- 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 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_4 : IsCofibrant.{v, u} X
inst_5 : IsCofibrant.{v, u} Y
f : X ⟶ Y
⊢ weakEquivalences (CofibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f

Tactic:
rfl
-- 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
X : C
inst_3 : IsCofibrant.{v, u} X
⊢ Eq.{v + 1} (α := Quiver.Hom (V := CofibrantObject.{v, u} C) (mk X) (mk X)) (homMk (𝟙 X)) (𝟙 (mk X))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- 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
X Y Z : C
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : IsCofibrant.{v, u} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Quiver.Hom (V := CofibrantObject.{v, u} C) (mk X) (mk Z))
    (CategoryStruct.comp (Y := mk Y) (homMk f) (homMk g)) (homMk (f ≫ g))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- 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
X : CofibrantObject.{v, u} C
⊢ IsCofibrant.{v, u} (X.obj (P := cofibrantObjects C))

Tactic:
X.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, HomotopicalAlgebra.cofibrantObjects
-- 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
X : CofibrantObject.{v, u} C
⊢ IsCofibrant.{v, u} (Functor.obj ι X)

Tactic:
X.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, HomotopicalAlgebra.cofibrantObjects
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
inst_3 : IsFibrant.{v, u} X
⊢ fibrantObjects.{v, u} C X

Tactic:
assumption
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : FibrantObject.{v, u} C
⊢ ∃ (Y : C) (x : IsFibrant.{v, u} Y), X = mk Y

Tactic:
⟨X.obj, X.property, rfl⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
X Y : C
inst_3 : IsFibrant.{v, u} X
inst_4 : IsFibrant.{v, u} Y
f : Quiver.Hom (V := FibrantObject.{v, u} C) (mk X) (mk Y)
⊢ ∃ (g : X ⟶ Y), f = homMk g

Tactic:
⟨f.hom, rfl⟩

Premises used: Exists.intro, CategoryTheory.InducedCategory.Hom.hom, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
simp : weakEquivalences (FibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f
⊢ WeakEquivalence (C := FibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
⊢ weakEquivalences (FibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
inst_3 : IsFibrant.{v, u} X
⊢ Eq.{v + 1} (α := Quiver.Hom (V := FibrantObject.{v, u} C) (mk X) (mk X)) (homMk (𝟙 X)) (𝟙 (mk X))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
X Y Z : C
inst_3 : IsFibrant.{v, u} X
inst_4 : IsFibrant.{v, u} Y
inst_5 : IsFibrant.{v, u} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Quiver.Hom (V := FibrantObject.{v, u} C) (mk X) (mk Z)) (CategoryStruct.comp (Y := mk Y) (homMk f) (homMk g))
    (homMk (f ≫ g))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : FibrantObject.{v, u} C
⊢ IsFibrant.{v, u} (X.obj (P := fibrantObjects C))

Tactic:
X.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, HomotopicalAlgebra.fibrantObjects
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : FibrantObject.{v, u} C
⊢ IsFibrant.{v, u} (Functor.obj ι X)

Tactic:
X.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, HomotopicalAlgebra.fibrantObjects
-- 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
⊢ LE.le (α := ObjectProperty.{v, u} C) (bifibrantObjects C) (cofibrantObjects C)

Tactic:
fun _ h ↦ h.1

Premises used: And.left
-- 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
⊢ LE.le (α := ObjectProperty.{v, u} C) (bifibrantObjects C) (fibrantObjects C)

Tactic:
fun _ h ↦ h.2

Premises used: And.right
-- 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 : C
inst_5 : IsCofibrant.{v, u} X
inst_6 : IsFibrant.{v, u} X
⊢ cofibrantObjects.{v, u} C X

Tactic:
assumption
-- 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 : C
inst_5 : IsCofibrant.{v, u} X
inst_6 : IsFibrant.{v, u} X
⊢ fibrantObjects.{v, u} C X

Tactic:
assumption
-- 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
⊢ ∃ (Y : C) (x : IsCofibrant.{v, u} Y) (x_1 : IsFibrant.{v, u} Y), X = mk Y

Tactic:
⟨X.obj, X.property.1, X.property.2, rfl⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, And.right, And.left, Exists.intro, rfl
-- 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 Y : C
inst_5 : IsCofibrant.{v, u} X
inst_6 : IsCofibrant.{v, u} Y
inst_7 : IsFibrant.{v, u} X
inst_8 : IsFibrant.{v, u} Y
f : Quiver.Hom (V := BifibrantObject.{v, u} C) (mk X) (mk Y)
⊢ ∃ (g : X ⟶ Y), f = homMk g

Tactic:
⟨f.hom, rfl⟩

Premises used: Exists.intro, CategoryTheory.InducedCategory.Hom.hom, rfl
-- 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
inst_5 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_6 : IsCofibrant.{v, u} X
inst_7 : IsFibrant.{v, u} X
inst_8 : IsCofibrant.{v, u} Y
inst_9 : IsFibrant.{v, u} Y
f : X ⟶ Y
simp : weakEquivalences (BifibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f
⊢ WeakEquivalence (C := BifibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- 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
inst_5 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_6 : IsCofibrant.{v, u} X
inst_7 : IsFibrant.{v, u} X
inst_8 : IsCofibrant.{v, u} Y
inst_9 : IsFibrant.{v, u} Y
f : X ⟶ Y
⊢ weakEquivalences (BifibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f

Tactic:
rfl
-- 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 : C
inst_5 : IsCofibrant.{v, u} X
inst_6 : IsFibrant.{v, u} X
⊢ Eq.{v + 1} (α := Quiver.Hom (V := BifibrantObject.{v, u} C) (mk X) (mk X)) (homMk (𝟙 X)) (𝟙 (mk X))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- 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 Y Z : C
inst_5 : IsCofibrant.{v, u} X
inst_6 : IsCofibrant.{v, u} Y
inst_7 : IsCofibrant.{v, u} Z
inst_8 : IsFibrant.{v, u} X
inst_9 : IsFibrant.{v, u} Y
inst_10 : IsFibrant.{v, u} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Quiver.Hom (V := BifibrantObject.{v, u} C) (mk X) (mk Z))
    (CategoryStruct.comp (Y := mk Y) (homMk f) (homMk g)) (homMk (f ≫ g))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- 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
⊢ IsCofibrant.{v, u} (X.obj (P := bifibrantObjects C))

Tactic:
X.property.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.left, HomotopicalAlgebra.cofibrantObjects
-- 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} (X.obj (P := bifibrantObjects C))

Tactic:
X.property.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.right, HomotopicalAlgebra.fibrantObjects
-- 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
⊢ IsCofibrant.{v, u} (Functor.obj ι X)

Tactic:
X.property.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.left, HomotopicalAlgebra.cofibrantObjects
-- 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 ι X)

Tactic:
X.property.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.right, HomotopicalAlgebra.fibrantObjects
-- 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
⊢ IsCofibrant.{v, u} ((Functor.obj ιFibrantObject X).obj (P := fibrantObjects C))

Tactic:
X.property.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.left, HomotopicalAlgebra.cofibrantObjects, HomotopicalAlgebra.bifibrantObjects, HomotopicalAlgebra.fibrantObjects