Formatting a math olympiad question in lean4

Stream: lean4

[lean_doubao]

I am new to the community. Does anybody know if the question below can be formatted in lean4?

---

Find all possible values of a, satisfying that the system x^2+20x+y^2 - 20y + 75 = |x^2 + y^2 - 25|, x - y = a has more than one solution. It's not a proof but just finding values of a.

[David Renshaw]

Here's how it might be formalized in the style of compfiles:

import Mathlib
import ProblemExtraction

/-!
Find all possible values of a, satisfying that the system

   x^2+20x+y^2 - 20y + 75 = |x^2 + y^2 - 25|
   x - y = a

has more than one solution.
-/

determine SolutionSet : Set ℝ := sorry

abbrev Equations (a x y : ℝ) : Prop :=
  x^2 + 20 * x + y^2 - 20 * y + 75 = |x^2 + y^2 - 25| ∧
  x - y = a

problem p1 (a : ℝ) :
    a ∈ SolutionSet ↔
    1 < {⟨x,y⟩ : ℝ×ℝ | Equations a x y}.encard := by
  sorry

[David Renshaw]

(The determine and problem commands are shallow wrappers of abbrev and theorem that are defined in ProblemExtraction.)