Lean not "seeing through" composition

Stream: mathlib4

[Arien Malec]

In mathlib4#1154, we have

def IsSMulRegular [SMul R M] (c : R) :=
  Function.Injective ((· • ·) c : M → M)

In theorem of_smul I had to simp [Function.comp] at cd to get Lean to understand that Function.comp (fun m ↦ a • m) ((fun x x_1 ↦ x • x_1) s) c = Function.comp (fun m ↦ a • m) ((fun x x_1 ↦ x • x_1) s) d was really a • s • c = a • s • d

Is this expected gymnastics?

[Kevin Buzzard]

If Function.comp is not reducible then it doesn't surprise me that you have to explicitly tell Lean to unfold it; I doubt it would choose to unfold it by itself. No doubt it's definitional though -- did you try dsimp only [Function.comp]? non-terminal simps are usually to be avoided.

[Arien Malec]

I guess it used to work before from the shape of the previous proof...

Will try dsimp only

[Kevin Buzzard]

Maybe

def IsSMulRegular [SMul R M] (c : R) :=
  Function.Injective ((c • ·) : M → M)

is a better definition?

[Kevin Buzzard]

But this doesn't solve the problem: it's the same issue as this (see discussion before for an explanation of why it might be hard to fix)

[Arien Malec]

Applied your suggestion(s), but as you note, doesn't solve the issue.

[Arien Malec]

Also seeing issues where simp only [one_mul] doesn't work, but simp [one_mul] does.

[Kevin Buzzard]

What does simp? [one_mul] say?

[Arien Malec]

@Eric Rodriguez pointed out that I wanted one_smul

[Arien Malec]

I think simp [one_mul] just simp'd everything away.

[Mario Carneiro]

the suggestion was simp? [one_mul], note the question mark

[Arien Malec]

Understood! I went back and looked and simp? [one_mul] wasn't helpful (suggested simp only).

[Arien Malec]

Same with simp?

[Kevin Buzzard]

that's annoying, I had hoped it would have pointed out that it was one_smul that you wanted.

[Eric Wieser]

Can we revert the statement to the mathlib3 spelling of

def IsSMulRegular [SMul R M] (c : R) :=
  Function.Injective (SMul.smul c : M → M)

which I expect makes this problem go away?

[Arien Malec]

It really doesn't. With that change, we get lots of stuff like a • SMul.smul s c = a • SMul.smul s d

[Arien Malec]

I tried reverting to the previous proofs, but then I've still got to do the dsimp trick. I've got the proofs as is to pretty clean rws after the dsimps.

[Eric Wieser]

Wait, Lean4 doesn't print SMul.smul a b as a • b any more!?

[Eric Wieser]

@Mario Carneiro, do you know if that is expected behavior?

[Eric Wieser]

Seems like it might be a problem for any of the proposed solutions to this problem that have come up so far

[Mario Carneiro]

no, it should be pretty printed

[Mario Carneiro]

there must be something off here, I would need a #mwe to diagnose

[Mario Carneiro]

note that SMul.smul a will probably not be pretty printed, although it could be pretty printed as (a • .) in principle

[Eric Wieser]

Yeah, i'm specifically worried about @Arien Malec's example above

[Arien Malec]

Let me see if I can minimize to an #mwe

[Arien Malec]

So I think

import Mathlib.Algebra.SmulWithZero
import Mathlib.Algebra.Regular.Basic

def IsSMulRegular [SMul R M] (c : R) :=
  Function.Injective (SMul.smul c : M → M)

namespace IsSMulRegular

variable {M}

variable [SMul R M] [SMul R S] [SMul S M] [IsScalarTower R S M]

theorem of_smul (a : R) (ab : IsSMulRegular M (a • s)) : IsSMulRegular M s :=
  @Function.Injective.of_comp _ _ _ (fun m : M => a • m) _ fun c d cd => by sorry

Gets you there.

[Arien Malec]

Putting the cursor after by, I get:

R: Type u_3
S: Type u_1
M: Type u_2
a✝b: R
s: S
inst✝³: SMul R M
inst✝²: SMul R S
inst✝¹: SMul S M
inst✝: IsScalarTower R S M
a: R
ab: IsSMulRegular M (a • s)
cd: M
cd: Function.comp (fun m ↦ a • m) (SMul.smul s) c = Function.comp (fun m ↦ a • m) (SMul.smul s) d
⊢ c = d

[Arien Malec]

Then

theorem of_smul (a : R) (ab : IsSMulRegular M (a • s)) : IsSMulRegular M s :=
  @Function.Injective.of_comp _ _ _ (fun m : M => a • m) _ fun c d cd => by
  dsimp only [Function.comp] at cd
  sorry

gets me

R: Type u_3
S: Type u_1
M: Type u_2
a✝b: R
s: S
inst✝³: SMul R M
inst✝²: SMul R S
inst✝¹: SMul S M
inst✝: IsScalarTower R S M
a: R
ab: IsSMulRegular M (a • s)
cd: M
cd: a • SMul.smul s c = a • SMul.smul s d
⊢ c = d

[Arien Malec]

And then I can't rw [←smul_assoc, ←smul_assoc] at cd