∀ (n : ℕ) (t : Set (ULift.{u_1, 0} ↑(Metric.closedBall 0 1))) (s : Set ↑(Metric.closedBall 0 1))
  (r : Set (EuclideanSpace ℝ (Fin n))),
  IsOpen r →
    Subtype.val ⁻¹' r = s →
      ULift.down ⁻¹' s = t →
        IsOpen
          ((fun x =>
              match x with
              | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ }) ⁻¹'
            t)