simp only [onFun, id_eq]
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ (fun a => a • s.mulStab) a ≠ (fun a => a • s.mulStab) b →
    (Disjoint on id) ((fun a => a • s.mulStab) a) ((fun a => a • s.mulStab) b)
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • s.mulStab ≠ b • s.mulStab → Disjoint (a • s.mulStab) (b • s.mulStab)