∀ {G : Type u_2} [inst : Group G] {α : Type u_1} [inst_1 : MulAction G α] {a : α} {n : ℕ}
  (x : Fin n ↪ ↥(SubMulAction.ofStabilizer G a)),
  a ∉ Set.range ⇑(x.trans (Function.Embedding.subtype fun x => x ∈ SubMulAction.ofStabilizer G a))