New puzzle: Find a number with a number of 4s and 7s that has only 4s and 7s

[akalai]

def sat(d: int):
    """
    Find a number bigger than n whose decimal representation has k 4's and 7's where k's decimal representation
    consists only of 4's and 7's

    Inspired by [Codeforces Problem 110 A](https://codeforces.com/problemset/problem/110/A)
    """
    return d > 123456789 and set(str(str(d).count("4") + str(d).count("7"))) <= {"4", "7"}

Solvers, post your solutions in the comments using the following formatting:

<details><summary>Reveal solution</summary>

```python
def sol():
    return "world"  # replace with your solution
```
</details>

[TalSchuster]

Reveal solution

def sol():
    return int("7" * int("4") + "1" * (len(str(123456789)) - int("4")))