Cardinal bounds for protected successors

theorem ScottishBook155.oneSum_mk_le_stageCardinal {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (hM : Cardinal.mk M ≤ stageCardinal) : Cardinal.mk (OneSum M) ≤ stageCardinal

theorem ScottishBook155.protectedSuccessor_source_mk_le {r L : ℝ} (hr : 0 < r) (hL : 0 < L) (S : ProtectedStage r) (y : S.target.carrier) (hy : y ∉ Set.range S.map) (hM : Cardinal.mk S.source.carrier ≤ stageCardinal) : Cardinal.mk (protectedSuccessor hr hL S y hy).next.source.carrier ≤ stageCardinal

theorem ScottishBook155.protectedSuccessor_target_mk_le {r L : ℝ} (hr : 0 < r) (hL : 0 < L) (S : ProtectedStage r) (y : S.target.carrier) (hy : y ∉ Set.range S.map) (hM : Cardinal.mk S.source.carrier ≤ stageCardinal) (hN : Cardinal.mk S.target.carrier ≤ stageCardinal) : Cardinal.mk (protectedSuccessor hr hL S y hy).next.target.carrier ≤ stageCardinal