mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case neg
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
h₃ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : weakEquivalences C g
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C f

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : weakEquivalences C g
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C f
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : weakEquivalences C f
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C g

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : weakEquivalences C f
hfg : weakEquivalences C (f ≫ g)
⊢ weakEquivalences C g
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to Y)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to Y)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).llp.IsStableUnderCobaseChange

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).llp.IsStableUnderCobaseChange
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to X ≫ i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to X ≫ i)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).rlp.IsStableUnderBaseChange

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).rlp.IsStableUnderBaseChange
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : Cofibration (initial.to Y)
⊢ Cofibration coprod.inl

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : Cofibration (initial.to Y)
⊢ Cofibration coprod.inl
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).llp.IsMultiplicative

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).llp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : cofibrations C (initial.to Y)
⊢ cofibrations C coprod.inl

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : cofibrations C (initial.to Y)
⊢ cofibrations C coprod.inl
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).rlp.IsMultiplicative

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).rlp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : Cofibration (initial.to X)
⊢ Cofibration coprod.inr

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : Cofibration (initial.to X)
⊢ Cofibration coprod.inr
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (fibrations C).llp.IsStableUnderCoproductsOfShape J

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (fibrations C).llp.IsStableUnderCoproductsOfShape J
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : cofibrations C (initial.to X)
⊢ cofibrations C coprod.inr

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : cofibrations C (initial.to X)
⊢ cofibrations C coprod.inr
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (trivialCofibrations C).rlp.IsStableUnderProductsOfShape J

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (trivialCofibrations C).rlp.IsStableUnderProductsOfShape J
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (trivialFibrations C).llp.IsStableUnderCobaseChange

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (trivialFibrations C).llp.IsStableUnderCobaseChange
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
inst✝¹ : (fibrations C).IsStableUnderComposition
X Y : C
p : X ⟶ Y
inst✝ : Fibration p
hY : Fibration (terminal.from Y)
⊢ Fibration (terminal.from X)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
inst✝¹ : (fibrations C).IsStableUnderComposition
X Y : C
p : X ⟶ Y
inst✝ : Fibration p
hY : Fibration (terminal.from Y)
⊢ Fibration (terminal.from X)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (cofibrations C).rlp.IsStableUnderBaseChange

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (cofibrations C).rlp.IsStableUnderBaseChange
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
inst✝¹ : (fibrations C).IsStableUnderComposition
X Y : C
p : X ⟶ Y
inst✝ : Fibration p
hY : Fibration (terminal.from Y)
⊢ Fibration (p ≫ terminal.from Y)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
inst✝¹ : (fibrations C).IsStableUnderComposition
X Y : C
p : X ⟶ Y
inst✝ : Fibration p
hY : Fibration (terminal.from Y)
⊢ Fibration (p ≫ terminal.from Y)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (trivialFibrations C).llp.IsMultiplicative

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (trivialFibrations C).llp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hY : Fibration (terminal.from Y)
⊢ Fibration prod.fst

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hY : Fibration (terminal.from Y)
⊢ Fibration prod.fst
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (cofibrations C).rlp.IsMultiplicative

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (cofibrations C).rlp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hY : fibrations C (terminal.from Y)
⊢ fibrations C prod.fst

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hY : fibrations C (terminal.from Y)
⊢ fibrations C prod.fst
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
J : Type w
⊢ (trivialFibrations C).llp.IsStableUnderCoproductsOfShape J

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
J : Type w
⊢ (trivialFibrations C).llp.IsStableUnderCoproductsOfShape J
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hX : Fibration (terminal.from X)
⊢ Fibration prod.snd

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hX : Fibration (terminal.from X)
⊢ Fibration prod.snd
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
J : Type w
⊢ (cofibrations C).rlp.IsStableUnderProductsOfShape J

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
J : Type w
⊢ (cofibrations C).rlp.IsStableUnderProductsOfShape J
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hX : fibrations C (terminal.from X)
⊢ fibrations C prod.snd

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hX : fibrations C (terminal.from X)
⊢ fibrations C prod.snd
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : (cofibrations C).IsStableUnderCobaseChange
hg : cofibrations C g
⊢ cofibrations C (pushout.inl f g)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : (cofibrations C).IsStableUnderCobaseChange
hg : cofibrations C g
⊢ cofibrations C (pushout.inl f g)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : (cofibrations C).IsStableUnderCobaseChange
hg : cofibrations C g
⊢ cofibrations C (pushout.inl f g)

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

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : (cofibrations C).IsStableUnderCobaseChange
hf : cofibrations C f
⊢ cofibrations C (pushout.inr f g)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : (cofibrations C).IsStableUnderCobaseChange
hf : cofibrations C f
⊢ cofibrations C (pushout.inr f g)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝³ : HasPushout f g
inst✝² : (trivialCofibrations C).IsStableUnderCobaseChange
inst✝¹ : Cofibration g
inst✝ : WeakEquivalence g
⊢ weakEquivalences C (pushout.inl f g)

Tactic:
]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝³ : HasPushout f g
inst✝² : (trivialCofibrations C).IsStableUnderCobaseChange
inst✝¹ : Cofibration g
inst✝ : WeakEquivalence g
⊢ weakEquivalences C (pushout.inl f g)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝³ : HasPushout f g
inst✝² : (trivialCofibrations C).IsStableUnderCobaseChange
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ weakEquivalences C (pushout.inr f g)

Tactic:
]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝³ : HasPushout f g
inst✝² : (trivialCofibrations C).IsStableUnderCobaseChange
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ weakEquivalences C (pushout.inr f g)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : (fibrations C).IsStableUnderBaseChange
hf : fibrations C f
⊢ fibrations C (pullback.snd f g)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : (fibrations C).IsStableUnderBaseChange
hf : fibrations C f
⊢ fibrations C (pullback.snd f g)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : (fibrations C).IsStableUnderBaseChange
hg : fibrations C g
⊢ fibrations C (pullback.fst f g)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : (fibrations C).IsStableUnderBaseChange
hg : fibrations C g
⊢ fibrations C (pullback.fst f g)