Lean4 typeclass tactic

Stream: lean4

[Won Seong]

Is there a useful tactic for proving instance in lean4? I think refine_struct would do the role in lean3, but I can't find any reference for lean4 and it seems that lean4 doesn't understand the tactic.

[Henrik Böving]

What kind of instance do you want to construct?

[Won Seong]

I want to construct an instance for module. I'm proving myself this fact
https://github.com/leanprover-community/mathlib4/blob/526457f3dc192dd9195993e0a48c9374b81af9c7/Mathlib/Algebra/Module/Basic.lean#L159-L165

[Won Seong]

While I don't understand the code in the link, I'm approaching in a more straightforward but tedious way. But using an instance expression like { smul := ... } doesn't seem like a good style.

[Won Seong]

Moreover it's good to fill the fields for the typeclass one by one for my copilot to autocomplete my code well.

[Henrik Böving]

we usually use the where syntax for instances when they are not being constructed in this fashion

[Won Seong]

image.png
I'm struggling here. How can I make the notation for 1 • b work? I need an instance HSMul R M M.

[Won Seong]

image.png
Is there any way to simplify this precoess?

[Eric Wieser]

Yes, your entire theorem is docs#Module.compHom

[Won Seong]

But the proofs don't use show clause. How can I construct instances during a proof and use a show clause?

[Eric Wieser]

Can you paste your code using #backticks above rather than an image?