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