Why won't rw see this?

Stream: new members

[Yan Yablonovskiy 🇺🇦]

I have been trying to figure out why this rw won't work:

import Mathlib.Algebra.Star.Basic

variable {M₂ : Type u} {α : Type u} [M : CommMonoid α]

postfix:100  "⋆" => Star.star

class abbrev InvolutionMonoid (α: Type u) := Monoid α, StarMul α

open Function in
def involutionmonoid [InvolutionMonoid α] [Mul M₂] [Pow M₂ ℕ] [Monoid M₂] [Star M₂]
    (f : α → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) (invol : ∀ x, f (x⋆) = (f x)⋆) : InvolutionMonoid M₂ where
  star_involutive := by
    rw [Involutive]
    intro x
    have (y : α) : f ( y⋆⋆ ) =  (f y)⋆⋆ := by simp only [invol]
    obtain ⟨⟨xₐₐinv,hxₐ⟩,xinv,hx⟩ := And.intro (hf (x⋆⋆)) (hf x)
    rw [←hx,←this xinv,star_involutive]
  star_mul x y := by
   have (x y : α) : f (x * y)⋆ =  f (y⋆) * f (x⋆) := by
    calc f (x * y)⋆ = f ((x * y)⋆) := (invol (x * y)).symm
    _ = f ( (y⋆) * (x⋆) ) := congrArg f (star_mul x y)
    _ = f (y⋆) * f (x⋆) := mul (y⋆) (x⋆)
   obtain ⟨⟨xinv,hx⟩,yinv,hy⟩ := And.intro (hf x) (hf y)
   rw [←hx,←hy,←invol xinv,←invol yinv]
   have := mul (yinv⋆) (xinv⋆)
   rw [←this]

Even in conv mode, isolating the term, it doesn't seem to recognise it and i can't seem to figure out why.

[Rado Kirov]

I don't know about the math involved here, but running into "surely this is the same expression" problems has been my most frustrating experience with Lean so far too, so I tried to see what's happening out of empathy for a fellow math formalizer :)

Started with the definition of * which looks identical, but if you further click on instHMul you will see two different instances.

Screenshot 2025-09-29 at 8.41.16 PM.png
Screenshot 2025-09-29 at 8.41.23 PM.png

Could this be cause of the problem? I have no idea how this happens and what to do next.

[Yan Yablonovskiy 🇺🇦]

Thank you! I couldn't find it. As to the math, it is a parallel of docs#Function.Surjective.monoid for involution monoids. As far as mathlib goes, this is like docs#StarAddMonoid but with multiplicative, mostly for practice. But also because the quotient space there builds up for rings and i am making a quotient space for something different.

[Damiano Testa]

You seem to have Mul M₂ and Monoid M₂ as your assumptions. These are going to be two completely unrelated multiplications on this type.

[Yan Yablonovskiy 🇺🇦]

Thank you so much, yes this was it!

[Damiano Testa]

I also suspect that Pow should not be there, as any monoid should already have a power by Nat.

[Rado Kirov]

Ah that makes sense, seems like simply removing [Mul \a] fixes the issue. Is it possible to imagine a better error message by Lean, so that one doesn't need to go around clicking every symbol to find the diff?

[Damiano Testa]

There was a discussion about improving this and I thought that Kyle had a more verbose error message. I'm not sure what the details were and if it should apply here.

[Damiano Testa]

The discussion that I had in mind was #lean4 dev > Misleading error message on type mismatch and, in particular, lean4#7172, which I realize now is a draft.