Open private and dot notation

Stream: lean4

[Jakob von Raumer]

Is there any good way around dot notation seemingly not being compatible with Batteries' open private?

import Batteries.Tactic.OpenPrivate

open Lean

open private Lean.ImportState.moduleNames from Lean.Environment

variable (s : ImportState)

#check s.moduleNames  -- Error: Field `moduleNames` from structure `Lean.ImportState` is private

#check Lean.ImportState.moduleNames s  -- works fine