English
If the cobase-change stability holds for trivial cofibrations, and g is a cofibration and a weak equivalence, then the left leg of the pushout is a weak equivalence.
Русский
Если устойчивость к cobase change для тривиальных кофибраций, и g — cofibration и слабая эквалентность, то левая стрелка пушаута — слабая эквалентность.
LaTeX
$$$[\\text{StableUnderCobaseChange}(\\mathrm{trivialCofibrations}(C))] [\\mathrm{Cofibration}(g)] [\\mathrm{WeakEquivalence}(g)] : \\mathrm{WeakEquivalence}(\\mathrm{pushout}.inl f g).$$$
Lean4
instance [(trivialCofibrations C).IsStableUnderCobaseChange] [Cofibration g] [WeakEquivalence g] :
WeakEquivalence (pushout.inl f g) := by
rw [weakEquivalence_iff]
exact (MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g) (mem_trivialCofibrations g)).2
