Unclear error "typeclass instance problem is stuck"

Stream: general

[ToMi]

I want to state a theorem saying that a function is a bijection. But for "(sigma_g g)" in "lemma sigma_g_bijective" I get "typeclass instance problem is stuck, it is often due to metavariables". Here's the code "```
import MIL.Common

open Function
open Equiv
open MulAction

variable {G A : Type*} [Group G] [MulAction G A]
variable {g : G}
variable {a : A}
-- Permutation repr. of an action is a homemorphism (Dummit & Foote p. 42)

def sigma_g (g : G) : A → A :=
fun a => g • a

lemma sigma_g_bijective : Bijective (sigma_g g) := by
sorry
```" What can be the reason for that? thanks

[Ruben Van de Velde]

There is no way for lean to know what A is

[Ruben Van de Velde]

And please note that the backticks should be on a line of their own

[ToMi]

Ok thanks. Any suggestions how handle testing the function for bijectivity?

[Ruben Van de Velde]

I think constructor will split into injective and surjective subgoals