simp only [foo] not working but simp [foo] works

Stream: mathlib4

[Arien Malec]

In mathlib4#1154 I have a couple of proofs that should be rw [foo] or simp only [foo] but I don't get closure except through simp [foo]

For example, in theorem one, I have

ab: 1 • a = 1 • b
⊢ a = b

which should be a simple rw [one_mul, one_mul] at ab but isn't because coercions? Here simp only [one_mul] at ab doesn't work, but simp [one_mul] at ab does.

Setting pp.all true

gives me the terrifying tactic state

ab: M
ab: @Eq.{u_2 + 1} M
  (@HSMul.hSMul.{u_1, u_2, u_2} R M M (@instHSMul.{u_1, u_2} R M (@MulAction.toSMul.{u_1, u_2} R M inst✝¹ inst✝))
    (@OfNat.ofNat.{u_1} R 1 (@One.toOfNat1.{u_1} R (@Monoid.toOne.{u_1} R inst✝¹))) a)
  (@HSMul.hSMul.{u_1, u_2, u_2} R M M (@instHSMul.{u_1, u_2} R M (@MulAction.toSMul.{u_1, u_2} R M inst✝¹ inst✝))
    (@OfNat.ofNat.{u_1} R 1 (@One.toOfNat1.{u_1} R (@Monoid.toOne.{u_1} R inst✝¹))) b)
⊢ @Eq.{u_2 + 1} M a b

[Kevin Buzzard]

I don't think you've been around long enough if you think that's terrifying. Didn't I post a 25 line pp.all output earlier today? ;-)

[Kevin Buzzard]

Try making the explicit one_mul term you want to rewrite using @one_mul and feeding in all the non-instances, and then compare.

[Arien Malec]

Well I've been exposed to C++ template errors, so nothing's really terrifying.

[Arien Malec]

Kevin Buzzard said:

Try making the explicit one_mul term you want to rewrite using @one_mul and feeding in all the non-instances, and then compare.

If I understand this, I'm getting issues where rw isn't seeing the full type applied to a here.

But I'm probably not understanding "feeding in all the non-instances"

application type mismatch
  @one_mul M a
argument
  a
has type
  M : Type u_2
but is expected to have type
  MulOneClass M : Type u_2

If I'm understanding correctly, a is MulAction which should give rw what it needs?

[Mario Carneiro]

there is a typeclass instance there, you should skip over it with @one_mul M _ a

[Arien Malec]

Making progress, now I'm at failed to synthesize instance MulOneClass M :-)

[Eric Rodriguez]

shouldn't it be rw [one_smul, one_smul]? or am I missing some detail

[Arien Malec]

Sometimes the obvious fix is the right one...