Success of `rw` depends on value of constant

Stream: general

[Eric Wieser]

I'm in a situation where using 1 in my defintion works, but using (⅟(2 : R)) does not:

import linear_algebra.tensor_algebra
import algebra.invertible

open free_algebra

variables (R : Type*) (M : Type*) [add_comm_group M] [comm_ring R] [invertible (2 : R)] [semimodule R M]

-- part of #4289, which breaks some things there
instance : ring (tensor_algebra R M) := algebra.semiring_to_ring R

variables {R M}

-- change (⅟(2 : R)) to 1 and the below `rw` works
def my_mul (a b : tensor_algebra R M) : tensor_algebra R M := (⅟(2 : R)) • (a * b - b * a)

lemma my_mul_assoc (a b c : tensor_algebra R M) : my_mul a (my_mul b c) = my_mul (my_mul a b) c :=
begin
  unfold my_mul,
  rw smul_sub, -- fails
  sorry
end

Why can lean only match smul_sub against 1 • (_ * _) and not ⅟ 2 • (_ * _)?

[Johan Commelin]

I don't really know... can you try feeding it the \frac1 2 as an explicit argument (in the rw)?

[Eric Wieser]

That fails too

[Eric Wieser]

Ah, a simpler reproduction: (1 : R) fails, 1 succeeds

[Johan Commelin]

Aha, so if you write 1, then it's the unit of the tensor algebra, I guess.

[Eric Wieser]

No, when I write 1 it's (1 : ℕ)

[Eric Wieser]

With (1 : ℕ), both the definition and proof find semimodule ℕ (tensor_algebra R M).
With (1 : R), the definition finds semimodule R (tensor_algebra R M) but the proof does not