Private lemmas on pointwise set ops appearing in simp?

Stream: mathlib4

[Yakov Pechersky]

MWE:

import Mathlib.Data.Set.Pointwise.Basic

example {α : Type*} [OrderedCommGroup α] {s : Set α} (h : BddBelow s) :
    BddAbove (s⁻¹) := by
  simp? -- Try this: simp only [_private.Mathlib.Data.Set.Pointwise.Basic.0.Set.involutiveInv._eq_1]
  sorry

[Alex J. Best]

I think this is the same lemma as https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20tracing.20suggests.20private.20simp.20theorems/near/406552591