{G : Type u_1} →
  [inst : Group G] →
    {α : Type u_2} →
      [inst_1 : MulAction G α] →
        {g : G} →
          {a b : α} →
            (hg : b = g • a) →
              ↥(SubMulAction.ofStabilizer G a) →ₑ[⇑(MulAction.stabilizerEquivStabilizer hg)]
                ↥(SubMulAction.ofStabilizer G b)