aesop? suggests unusable _private.Mathlib.Data.Set.Pointwise.Basic.0.Set.involutiveNeg._eq_1

[adomasbaliuka]

import Mathlib

lemma zero_mem_iff_zero_mem_neg (U : Set ℝ)
    : 0 ∈ U ↔ 0 ∈ -U := by
   aesop?
   -- simp_all only [Set.mem_neg, neg_zero] -- this solves it
   -- aesop? output for me has another unusable lemma:
   -- simp_all only [_private.Mathlib.Data.Set.Pointwise.Basic.0.Set.involutiveNeg._eq_1, Set.mem_neg, neg_zero]

[JLimperg]

Thanks for reporting! This is either a core issue or a to_additive issue. Minimisation:

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]

[JLimperg]

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20tracing.20suggests.20private.20simp.20theorems