Kourovka/1_74: `kourovka_1_74` asks for one topologized Tarski monster, not all Platonov-minimal groups

`Kourovka.«1.74».kourovka_1_74` asks only whether some Tarski monster admits a non-discrete Hausdorff group topology, whereas Problem 1.74 asks to describe all Platonov-minimal topological groups, those non-discrete Hausdorff groups whose proper closed subgroups are all discrete, a class that is not exhausted by Tarski monsters (the additive real line belongs to it) and that no declaration in the file characterizes.

https://tadamcz.com/fc-review-results/c90271f0fa/#/f/Kourovka/1_74

- 1 misformalization
- 1 status issue
- 1 equivalent reformulation
- trivial proof: bailed out
- fix compiles

_{Found by a language-model audit of the repository at c90271f0fa. Not reviewed by a human. This issue's title and description were written by a language model as well.}

Start at the Kourovka/1_74 declaration and compare it with the statement of Problem 1.74. Replace the Tarski-monster-only formulation with the intended characterization of all Platonov-minimal topological groups, then run the affected Lean checks to confirm the declaration compiles.

Written by the indexing model from the issue text.