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