simp tracing suggests private simp theorems

Stream: lean4

[Jannis Limperg]

This is a minimisation of aesop#89, where simp_all? includes a private equation lemma in the simp only list.

In Mathlib/Min1.lean:

import Mathlib.Tactic.ToAdditive

class Inv (α : Type _) where
  /-- Invert an element of α. -/
  inv : α → α

postfix:max "⁻¹" => Inv.inv

class InvolutiveInv (G : Type _) extends Inv G where
  protected inv_inv : ∀ x : G, x⁻¹⁻¹ = x

def Set (α : Type _) := α → Prop

instance {α} : Membership α (Set α) := sorry

@[to_additive (attr := simp)]
noncomputable instance involutiveInv {α} [InvolutiveInv α] : InvolutiveInv (Set α) where
  inv := sorry
  inv_inv s := sorry

structure Real where

instance : InvolutiveInv Real := sorry
instance {n} : OfNat Real n := sorry

In Min.lean:

import Mathlib.Min1

theorem zero_mem_iff_zero_mem_neg (U : Set Real)
    : 0 ∈ U ↔ 0 ∈ U⁻¹ := by
  set_option tactic.simp.trace true in
  simp_all
  -- Try this: simp_all only [_private.Mathlib.Min1.0.involutiveNeg._eq_1]

The simp_all only suggestion obviously can't work, but I'm not sure who the culprit is. Is there an expectation that the simp database doesn't contain private theorems? If so, to_additive probably needs fixing. If not, how should simp tracing deal with these private theorems?