awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : WeakEquivalence g
hfg : WeakEquivalence (f ≫ g)
rw : ∀ (hg : weakEquivalences C g) (hfg : weakEquivalences C (f ≫ g)), weakEquivalences C f
⊢ WeakEquivalence f

Tactic:
rw [weakEquivalence_iff] at hg hfg ⊢

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : weakEquivalences C g
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C f

Tactic:
of_postcomp _ _ _ hg hfg

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : weakEquivalences C g
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C f

Tactic:
exact of_postcomp _ _ _ hg hfg

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : WeakEquivalence f
hfg : WeakEquivalence (f ≫ g)
rw : ∀ (hf : weakEquivalences C f) (hfg : weakEquivalences C (f ≫ g)), weakEquivalences C g
⊢ WeakEquivalence g

Tactic:
rw [weakEquivalence_iff] at hf hfg ⊢

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : weakEquivalences C f
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C g

Tactic:
of_precomp _ _ _ hf hfg

Premises used: CategoryTheory.MorphismProperty.of_precomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : weakEquivalences C f
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C g

Tactic:
exact of_precomp _ _ _ hf hfg

Premises used: CategoryTheory.MorphismProperty.of_precomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : WeakEquivalence g
⊢ WeakEquivalence (f ≫ g) ↔ WeakEquivalence f

Tactic:
⟨fun _ ↦ weakEquivalence_of_postcomp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, HomotopicalAlgebra.weakEquivalence_of_postcomp, Iff.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : WeakEquivalence f
⊢ WeakEquivalence (f ≫ g) ↔ WeakEquivalence g

Tactic:
⟨fun _ ↦ weakEquivalence_of_precomp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, HomotopicalAlgebra.weakEquivalence_of_precomp, Iff.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst_3 : WeakEquivalence g
hfg : WeakEquivalence fg
⊢ WeakEquivalence (f ≫ g)

Tactic:
subst fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : WeakEquivalence g
hfg : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence f

Tactic:
weakEquivalence_of_postcomp f g

Premises used: HomotopicalAlgebra.weakEquivalence_of_postcomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : WeakEquivalence g
hfg : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence f

Tactic:
exact weakEquivalence_of_postcomp f g

Premises used: HomotopicalAlgebra.weakEquivalence_of_postcomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst_3 : WeakEquivalence f
inst_4 : WeakEquivalence fg
⊢ WeakEquivalence (f ≫ g)

Tactic:
subst fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : WeakEquivalence f
inst_4 : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence g

Tactic:
weakEquivalence_of_precomp f g

Premises used: HomotopicalAlgebra.weakEquivalence_of_precomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : WeakEquivalence f
inst_4 : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence g

Tactic:
exact weakEquivalence_of_precomp f g

Premises used: HomotopicalAlgebra.weakEquivalence_of_precomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ Eq (α := MorphismProperty.{v, u} C) (llp (fibrations C)) (trivialCofibrations C)

Tactic:
llp_eq_of_wfs _ _

Premises used: CategoryTheory.MorphismProperty.llp_eq_of_wfs
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ Eq (α := MorphismProperty.{v, u} C) (rlp (trivialCofibrations C)) (fibrations C)

Tactic:
rlp_eq_of_wfs _ _

Premises used: CategoryTheory.MorphismProperty.rlp_eq_of_wfs
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
rw : IsStableUnderCobaseChange.{v, u} (llp (fibrations C))
⊢ IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)

Tactic:
rw [← fibrations_llp]

Premises used: HomotopicalAlgebra.fibrations_llp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderCobaseChange.{v, u} (llp (fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
rw : IsStableUnderBaseChange.{v, u} (rlp (trivialCofibrations C))
⊢ IsStableUnderBaseChange.{v, u} (fibrations C)

Tactic:
rw [← trivialCofibrations_rlp]

Premises used: HomotopicalAlgebra.trivialCofibrations_rlp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderBaseChange.{v, u} (rlp (trivialCofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
rw : IsMultiplicative.{v, u} (llp (fibrations C))
⊢ IsMultiplicative.{v, u} (trivialCofibrations C)

Tactic:
rw [← fibrations_llp]

Premises used: HomotopicalAlgebra.fibrations_llp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsMultiplicative.{v, u} (llp (fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
rw : IsMultiplicative.{v, u} (rlp (trivialCofibrations C))
⊢ IsMultiplicative.{v, u} (fibrations C)

Tactic:
rw [← trivialCofibrations_rlp]

Premises used: HomotopicalAlgebra.trivialCofibrations_rlp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsMultiplicative.{v, u} (rlp (trivialCofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
J : Type w
rw : IsStableUnderCoproductsOfShape.{v, u, w} (llp (fibrations C)) J
⊢ IsStableUnderCoproductsOfShape.{v, u, w} (trivialCofibrations C) J

Tactic:
rw [← fibrations_llp]

Premises used: HomotopicalAlgebra.fibrations_llp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
J : Type w
⊢ IsStableUnderCoproductsOfShape.{v, u, w} (llp (fibrations C)) J

Tactic:
apply MorphismProperty.llp_isStableUnderCoproductsOfShape

Premises used: CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
J : Type w
rw : IsStableUnderProductsOfShape.{v, u, w} (rlp (trivialCofibrations C)) J
⊢ IsStableUnderProductsOfShape.{v, u, w} (fibrations C) J

Tactic:
rw [← trivialCofibrations_rlp]

Premises used: HomotopicalAlgebra.trivialCofibrations_rlp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
J : Type w
⊢ IsStableUnderProductsOfShape.{v, u, w} (rlp (trivialCofibrations C)) J

Tactic:
apply MorphismProperty.rlp_isStableUnderProductsOfShape

Premises used: CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ Eq (α := MorphismProperty.{v, u} C) (llp (trivialFibrations C)) (cofibrations C)

Tactic:
llp_eq_of_wfs _ _

Premises used: CategoryTheory.MorphismProperty.llp_eq_of_wfs
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ Eq (α := MorphismProperty.{v, u} C) (rlp (cofibrations C)) (trivialFibrations C)

Tactic:
rlp_eq_of_wfs _ _

Premises used: CategoryTheory.MorphismProperty.rlp_eq_of_wfs
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
rw : IsStableUnderCobaseChange.{v, u} (llp (trivialFibrations C))
⊢ IsStableUnderCobaseChange.{v, u} (cofibrations C)

Tactic:
rw [← trivialFibrations_llp]

Premises used: HomotopicalAlgebra.trivialFibrations_llp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsStableUnderCobaseChange.{v, u} (llp (trivialFibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
rw : IsStableUnderBaseChange.{v, u} (rlp (cofibrations C))
⊢ IsStableUnderBaseChange.{v, u} (trivialFibrations C)

Tactic:
rw [← cofibrations_rlp]

Premises used: HomotopicalAlgebra.cofibrations_rlp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsStableUnderBaseChange.{v, u} (rlp (cofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
rw : IsMultiplicative.{v, u} (llp (trivialFibrations C))
⊢ IsMultiplicative.{v, u} (cofibrations C)

Tactic:
rw [← trivialFibrations_llp]

Premises used: HomotopicalAlgebra.trivialFibrations_llp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsMultiplicative.{v, u} (llp (trivialFibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
rw : IsMultiplicative.{v, u} (rlp (cofibrations C))
⊢ IsMultiplicative.{v, u} (trivialFibrations C)

Tactic:
rw [← cofibrations_rlp]

Premises used: HomotopicalAlgebra.cofibrations_rlp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsMultiplicative.{v, u} (rlp (cofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
J : Type w
rw : IsStableUnderCoproductsOfShape.{v, u, w} (llp (trivialFibrations C)) J
⊢ IsStableUnderCoproductsOfShape.{v, u, w} (cofibrations C) J

Tactic:
rw [← trivialFibrations_llp]

Premises used: HomotopicalAlgebra.trivialFibrations_llp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
J : Type w
⊢ IsStableUnderCoproductsOfShape.{v, u, w} (llp (trivialFibrations C)) J

Tactic:
apply MorphismProperty.llp_isStableUnderCoproductsOfShape

Premises used: CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
J : Type w
rw : IsStableUnderProductsOfShape.{v, u, w} (rlp (cofibrations C)) J
⊢ IsStableUnderProductsOfShape.{v, u, w} (trivialFibrations C) J

Tactic:
rw [← cofibrations_rlp]

Premises used: HomotopicalAlgebra.cofibrations_rlp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
J : Type w
⊢ IsStableUnderProductsOfShape.{v, u, w} (rlp (cofibrations C)) J

Tactic:
apply MorphismProperty.rlp_isStableUnderProductsOfShape

Premises used: CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hg : Cofibration g
rw : ∀ (hg : cofibrations C g), cofibrations C (Y := pushout f g) (pushout.inl f g)
⊢ Cofibration (Y := pushout f g) (pushout.inl f g)

Tactic:
rw [cofibration_iff] at hg ⊢

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hg : cofibrations C g
⊢ cofibrations C (Y := pushout f g) (pushout.inl f g)

Tactic:
MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g) hg

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hg : cofibrations C g
⊢ cofibrations C (Y := pushout f g) (pushout.inl f g)

Tactic:
exact MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g) hg

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hf : Cofibration f
rw : ∀ (hf : cofibrations C f), cofibrations C (Y := pushout f g) (pushout.inr f g)
⊢ Cofibration (Y := pushout f g) (pushout.inr f g)

Tactic:
rw [cofibration_iff] at hf ⊢

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hf : cofibrations C f
⊢ cofibrations C (Y := pushout f g) (pushout.inr f g)

Tactic:
MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g).flip hf

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout, CategoryTheory.IsPushout.flip
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hf : cofibrations C f
⊢ cofibrations C (Y := pushout f g) (pushout.inr f g)

Tactic:
exact MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g).flip hf

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout, CategoryTheory.IsPushout.flip
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration g
inst_7 : WeakEquivalence g
rw : weakEquivalences C (Y := pushout f g) (pushout.inl f g)
⊢ WeakEquivalence (Y := pushout f g) (pushout.inl f g)

Tactic:
rw [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff