[PRQ#70090] Orphan Request for lean4