In Beilinson-Drinfeld (Hitchin System, lemma (362)) they show that if f:X->Y is a morphism between formally smooth ind-schemes of ind-finite type such that the differential is surjective then f is formally smooth.
My question is if this lemma is still true is we replace Y by the quotient stack [G(O)\G(F)/G(O)] and X as before, if the differential is surjective, do we have that that f is formally smooth?
Here F is k((t)) and O is ring of integers. G semisimple. N.B: All the ind-schemes here are ind-schemes for countable inductive systems.