∀ (S : Type u_1) [inst : SeminormedAddGroup S] [inst_1 : IsUltrametricDist S] {r : ℝ} (hr : 0 < r),
  IsUltrametricDist.closedBall_openAddSubgroup S hr =
    { carrier := Metric.closedBall 0 r, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, isOpen' := ⋯ }