Open adomasbaliuka opened 7 months ago
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]